프로멜라

이 기사는 대체로 또는 전적으로 단일 출처에 의존한다. 관련 토론은 토크 페이지에서 찾을 수 있다. 추가 출처에 인용구를 도입하여 이 기사를 개선할 수 있도록 도와주십시오. 출처 찾기: "Promela" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2014년 7월)

PROMELA(Process or Protocol Meta Language)는 Gerard J. Holzmann이 도입한 검증 모델링 언어다.언어는 예를 들어 분산형 시스템을 모델링할 동시 프로세스를 동적으로 만들 수 있도록 한다.PROMELA 모델에서 메시지 채널을 통한 통신은 동기(즉, 랑데부) 또는 비동기(즉, 버퍼링)로 정의할 수 있다.PROMELA 모델은 SPIN 모델 체커를 통해 분석하여 모델링된 시스템이 원하는 동작을 생성하는지 확인할 수 있다.Automata의 Computer Aided Verification 프로젝트의 일환으로 Isabelle/HOL로 검증된 구현도 이용할 수 있다.^[1]Promela에서 작성된 파일은 전통적으로.pml 파일 확장자

소개

PROMELA는 병렬 시스템의 논리를 검증하는 데 사용되는 프로세스 모델링 언어다.PROMELA의 프로그램이 주어지는 경우, Spin은 모델링된 시스템 실행의 무작위 또는 반복 시뮬레이션을 수행함으로써 모델의 정확성을 검증할 수 있으며, 시스템 상태 공간의 신속한 철저한 검증을 수행하는 C 프로그램을 생성할 수 있다.시뮬레이션 및 검증 중에 SPIN은 교착 상태, 지정되지 않은 수신 및 불가해한 코드의 부재를 점검한다.검증자는 또한 시스템 불변제의 정확성을 입증하는 데 사용될 수 있으며 비진행 실행 주기를 찾을 수 있다.마지막으로, 그것은 Promela never-claims로 또는 시간적 논리의 제약조건을 직접 형성함으로써 선형 시간적 제약조건의 검증을 지원한다.각 모델은 환경에 대한 다양한 유형의 가정 하에서 스핀을 사용하여 검증할 수 있다.일단 스핀으로 모델의 정확성이 확립되면, 그 사실은 이후의 모든 모델의 구성과 검증에 이용될 수 있다.

PROMELA 프로그램은 프로세스, 메시지 채널, 변수로 구성된다.프로세스는 분산 시스템의 동시 엔티티를 나타내는 글로벌 개체다.메시지 채널 및 변수는 프로세스 내에서 전역 또는 로컬로 선언할 수 있다.프로세스는 행동을 지정하고, 채널 및 글로벌 변수는 프로세스가 실행되는 환경을 정의한다.

언어참조

데이터 유형

PROMELA에서 사용되는 기본 데이터 유형은 아래 표에 제시되어 있다.PC i386/리눅스 기계의 크기는 비트 단위로 지정된다.

그 이름들bit그리고bool하나의 정보에 대한 동의어 입니다.abyte0에서 255 사이의 값을 저장할 수 있는 서명되지 않은 수량. 반바지 및ints는 보유할 수 있는 값의 범위에서만 다른 서명된 수량이다.

변수는 배열로도 선언할 수 있다.예를 들어 선언:

 인트로 x [10]; 

다음과 같은 배열 첨자 식에서 액세스할 수 있는 10개의 정수의 배열을 선언한다.

x[0] = x[1] + x[2];

그러나 배열은 생성 시 열거할 수 없으므로 다음과 같이 초기화해야 한다.

 인트로 x[3];  x[0] = 1;  x[1] = 2;  x[2] = 3; 

배열의 인덱스는 고유한 정수 값을 결정하는 표현식이 될 수 있다.범위를 벗어난 지수의 효과는 정의되지 않는다.다차원 배열은 의 도움을 받아 간접적으로 정의할 수 있다.typedef구성하다(아래 참조).

과정

변수 또는 메시지 채널의 상태는 프로세스별로만 변경 또는 검사할 수 있다.프로세스의 동작은 형식 선언에 의해 정의된다.예를 들어, 다음은 하나의 변수 상태를 가진 프로세스 유형 A를 선언한다.

A() {바이트 상태, 상태 = 3; }

Proctype 정의는 프로세스 동작을 선언할 뿐 실행하지 않는다.처음에 PROMELA 모델에서는 모든 PROMELA 규격에 명시적으로 선언되어야 하는 형식 초기화 프로세스, 즉 하나의 프로세스만 실행될 것이다.

새로운 프로세스는 실행문을 사용하여 생성될 수 있으며, 실행문은 프록타입의 이름으로 구성된 인수를 사용하여 프로세스에서 인스턴스화된다.실행 연산자는 초기 프로세스뿐만 아니라 프록터형 정의 본문에서 사용될 수 있다.이를 통해 PROMela에서 프로세스를 동적으로 생성할 수 있다.

실행 프로세스는 종료될 때 사라진다. 즉, 프로텍터형 정의에서 신체의 끝에 도달하고, 시작했던 모든 하위 프로세스가 종료되었을 때.

프록타입도 활성(아래)일 수 있다.

원자구축

키워드와 함께 곱슬 브레이스로 둘러싸인 일련의 문 앞에 접두사 붙임atomic사용자는 시퀀스가 다른 프로세스와 상호 교환되지 않은 하나의 분리할 수 없는 단위로 실행되어야 함을 나타낼 수 있다.

원자성 {문; }

원자 시퀀스는 검증 모델의 복잡성을 줄이는 중요한 도구가 될 수 있다.원자 시퀀스는 분산 시스템에서 허용되는 인터리빙의 양을 제한한다는 점에 유의하십시오.난치성 모델은 원자 염기서열로 국소 변수의 모든 조작에 라벨을 붙임으로써 다루기 쉽게 만들 수 있다.

메시지 전달

메시지 채널은 한 프로세스에서 다른 프로세스로의 데이터 전송을 모델링하는 데 사용된다.예를 들어 다음과 같이 로컬 또는 전역으로 선언된다.

chan qname = {short}의 [16]

이것은 타입 쇼트(여기는 용량이 16이다)의 메시지를 최대 16개까지 저장할 수 있는 버퍼링된 채널을 선언한다.

성명서:

qname! expr;

qname이라는 이름의 채널로 표현식 expr 값을 전송한다. 즉, 채널의 꼬리에 값을 추가한다.

성명서:

qname ?msg;

메시지를 수신하여 채널 헤드에서 검색한 후 변수 msg에 저장한다.그 채널들은 메시지를 선착순으로 전달한다.

랑데부 포트는 저장 길이가 0인 메시지 채널로 선언할 수 있다.예를 들어 다음과 같다.

chan 포트 = {byte}의 [0]개

유형별 메시지를 전달할 수 있는 랑데부 포트를 정의한다.byte그러한 랑데부 포트를 통한 메시지 상호작용은 정의상 동기식이다. 즉, 송신자 또는 수신자(채널에 가장 먼저 도착하는 수신자 또는 송신자)는 두 번째로 도착하는 경쟁자를 차단한다.

버퍼링된 채널이 용량으로 채워졌을 때(입력 수신에 앞서 "용량" 출력 수를 전송하는 경우), 채널의 기본 동작은 동기화가 되고, 송신자는 다음 송신에서 차단된다.채널 간에 공유되는 공통 메시지 버퍼가 없는지 확인하십시오.채널을 단방향 및 지점간으로 사용하는 것에 비해 복잡성이 증가함에 따라, 복수의 수신자 또는 복수의 송신자 간에 채널을 공유하고, 독립된 데이터 스트림을 하나의 공유 채널로 통합하는 것이 가능하다.이로부터 양방향 통신에도 단일 채널을 사용할 수 있다.

제어 흐름 구성

PROMELA에는 세 가지 제어 흐름 구조가 있다.그들은 사례 선택, 반복, 그리고 무조건적인 점프다.

사례 선택

가장 간단한 구조는 선택 구조다.예를 들어, 두 변수 a와 b의 상대적 값을 사용하여 다음과 같이 쓸 수 있다.

if : (a != b) -> 옵션1 : (a == b) -> 옵션2 fi

선택 구조에는 각각 이중 대장(double colon)이 선행하는 2개의 실행 순서가 있다.리스트에서 한 시퀀스가 실행될 것이다.시퀀스는 첫 번째 문이 실행 가능한 경우에만 선택할 수 있다.제어 시퀀스의 첫 번째 문장은 가드라고 불린다.

위의 예에서 경비원은 상호 배타적이지만 그럴 필요는 없다.둘 이상의 가드가 실행 가능한 경우 해당 시퀀스 중 하나가 비결정적으로 선택된다.모든 경비원이 불가항력적인 경우, 그 중 하나를 선택할 수 있을 때까지 프로세스가 차단된다.(반대, 어떤 실행 가능한 경비원에서도 오캄 프로그래밍 언어가 중단되거나 진행되지 않을 것이다.)

만약 : (A == true) -> 옵션1; : (B == true) -> 옵션2; /* A===true */ : : 다른 -> fallthrough_option; fi도 여기에 도착할 수 있다.

비결정론적 선택의 결과는 위의 예에서 A가 참일 경우 두 가지 선택을 모두 취할 수 있다."전통적인" 프로그래밍에서는 if - if -가 순차적으로 구조를 이해한다.여기서 if - double colon - double colon은 "준비된 모든 사람"으로 이해되어야 하며, 준비가 되어 있지 않으면 다른 대장은 그 때에만 취해질 것이다.

if : : 값 = 3; : : 값 = 4; fi

위의 예에서 값은 결정적으로 3 또는 4가 주어지지 않는다.

가드로 사용할 수 있는 두 가지 사이비 진술이 있는데, 시간 초과 문장과 다른 문장이 그것이다.시간 초과 문장은 프로세스가 결코 진실이 아닐 수 있는 조건을 기다리는 것을 중단할 수 있도록 하는 특수 조건을 모델링한다.다른 문은 선택 또는 반복 문에서 마지막 옵션 시퀀스의 초기 문으로 사용할 수 있다.다른 하나는 동일한 선택 항목의 다른 모든 옵션이 실행 가능하지 않은 경우에만 실행 가능한 것이다.또한 다른 것은 채널과 함께 사용하지 않을 수도 있다.

반복(루프)

선택 구조의 논리적 확장은 반복 구조다.예를 들면 다음과 같다.

do : : count = count + 1 : a = b + 2 : (count == 0) -> break od

PROMela에서 반복 구조를 설명한다.한 번에 하나의 옵션만 선택할 수 있다.옵션이 완료된 후 구조물의 실행이 반복된다.반복 구조를 종료하는 일반적인 방법은 브레이크 문구를 사용하는 것이다.그것은 반복 구조를 즉시 따르는 지시로 통제권을 이전한다.

무조건 점프

고리를 끊는 또 다른 방법은goto명세서예를 들어 위의 예를 다음과 같이 수정할 수 있다.

do : : : count = count + 1 : a = b + 2 : (count == 0) -> done done done: skip;

이 예에서 goto는 done이라는 이름의 라벨로 점프한다.라벨은 문 앞에만 나타날 수 있다.예를 들어, 프로그램의 끝에서 점프하는 것은 더미 문 스킵이 유용하다: 항상 실행 가능하고 아무런 효과도 없는 플레이스홀더다.

주장

PROMela에서 약간의 설명이 필요한 중요한 언어구조는 단언이다.양식의 문장:

어설션(any_boolean_condition)

항상 실행 가능하다.지정된 부울 조건이 유지되면 문에는 아무런 영향이 없다.그러나 조건이 반드시 유지되지 않는 경우, 이 문장은 스핀으로 검증하는 동안 오류를 발생시킬 것이다.

복잡한 데이터 구조

A PROMELAtypedef 정의를 사용하여 미리 정의된 또는 이전에 정의된 유형의 데이터 개체 목록에 대한 새 이름을 도입할 수 있다.새로운 유형 이름은 새로운 데이터 객체를 선언하고 인스턴스화하는 데 사용될 수 있으며, 이는 다음과 같은 분명한 방법으로 어떤 맥락에서든 사용될 수 있다.

 타이피프 마이스트락트  {      키가 작은 필드1;      바이트  필드2;  }; 

typef 구성으로 선언된 필드에 대한 액세스는 C 프로그래밍 언어와 동일한 방식으로 수행된다.예를 들면 다음과 같다.

MyStruct x; x.필드1 = 1;

유효한 PROMELA 시퀀스로 변수 x 값 1의 필드1에 할당된다.

활성 프락티페스

그active키워드는 모든 형식 정의 앞에 붙일 수 있다.키워드가 있으면 해당 프록타입의 인스턴스가 초기 시스템 상태에서 활성화된다.해당 유형의 다중 인스턴스화는 키워드의 선택적 배열 접미사로 지정할 수 있다.예:

활성 프록타입 A() { ...} 활성 [4] Proctype B() { ...}

실행 가능성

실행가능성의 의미론은 Promela에서 프로세스 동기화를 모델링하기 위한 기본 수단을 제공한다.

Mtype={M_UP, M_DW},{mtype}의 chan Chan_data_down)[0];{mtype}의 chan Chan_data_up)[0];proctype P1(chan Chan_data_in, Chan_data_out){::니 Chan_data_in?M_UP ->, 스킵>::Chan_data_out!M_DW ->, 스킵;니다.};proctype P2(chan Chan_data_in, Chan_data_out){니::Chan_data_in?M_DW ->, 스킵>::.Chan_data_out! M_UP -> 스킵; od; od; {원자성 { run P1(Chan_data_up, Chan_data_data_data_down), 실행 P2(Chan_data_down, Chan_data_up); }}

이 예에서, 두 공정 P1과 P2는 (1) 입력의 비결정론적 선택 또는 (2) 출력에서 다른 입력으로 선택한다.두 번의 랑데부 악수, 즉 실행이 가능하며, 그 중 하나를 선택한다.이것은 영원히 반복된다.따라서 이 모델은 교착상태에 빠지지 않을 것이다.

스핀은 위와 같은 모델을 분석하면, 모든 실행 가능한 선택이 탐색되는 비결정론적 알고리즘으로 선택지를 검증한다.그러나 Spin의 시뮬레이터가 가능한 검증되지 않은 통신 패턴을 시각화할 때 "비결정론적" 선택을 해결하기 위해 무작위 발생기를 사용할 수 있다.따라서 시뮬레이터가 나쁜 실행을 보여주지 못할 수 있다(예: 나쁜 추적은 없다).이는 검증과 시뮬레이션의 차이를 보여준다.또한 정교함을 이용하여 Promela 모델에서 실행 가능한 코드를 생성할 수도 있다.^[2]

키워드

다음 식별자는 키워드로 사용하기 위해 예약되어 있다.

참조

외부 링크

• 스핀 홈페이지
• 스핀 자습서 및 온라인 참조
• 간결한 Promela 참조 자료