Promela 간단한 시작 자습서

최근에는 코드의 논리를 감지하기 위해 Promela 언어를 사용하고 개발하고 있습니다.
Promela는 사용하기가 매우 번거롭지만, 인터넷에 Windows GUI 프로그램이 있는데, 그 안에는 많은 예 코드가 포함되어 있어, 조금만 보면 알 수 있다
도구 이름은 JSpin입니다.
https://code.google.com/p/jspin/
설치는 간단합니다. 설치한 후에 설치 디렉터리에 있는 config 파일을 열어 Mingw 경로를 설정하면 됩니다.
프로그램을 켜서 실행하고, 예시 코드를 아무렇게나 찾아서 뛰어내린다. 만약 컴파일에 성공하지 못하면, 그의 런에 있다.bat 앞에 이 줄을 붙여주세요.
SET PATH=%path%;c:/path_of_mingw/bin
설치 디렉터리에서 사용자 매뉴얼 jspin-user를 찾을 수 있습니다.pdf
일반 검측 및 발신 코드는 아래 세 가지를 검측해야 한다
1. 상호 배척(Mutual exclusion)
2. 잠금 해제(Free from Deadlock)
3. 배고픔 없음(Free from starvation)
이 도구에서 assert () 로 검사할 수도 있고 LTL (선형 시간 논리) 을 직접 써서 검사할 수도 있습니다.
너는 안에 있는dekker를 열 수 있다.pml에서 그것들을 어떻게 사용해서 검사하는지 배워라
pml 언어의 문법은 약간 기발하지만, 보면 active proctype은 하나의 라인을 설명하는 것이다

/* Dekker's algorithm */
bool    wantp = false, wantq = false;
byte    turn = 1;
bool csp = false, csq = false;

ltl { []<>csp && []<>csq }

active proctype p() {
    do
    ::  wantp = true;
        do
        :: !wantq -> break;
        :: else ->
            if
            :: (turn == 1)
            :: (turn == 2) ->
                wantp = false;
                (turn == 1);
                wantp = true
            fi
        od;
        csp = true;
        assert (!(csp && csq));
        csp = false;
        wantp = false;
        turn = 2
    od
}

active proctype q() {
    do
    ::  wantq = true;
        do
        :: !wantp -> break;
        :: else ->
            if
            :: (turn == 2)
            :: (turn == 1) ->
                wantq = false;
                (turn == 2);
                wantq = true
            fi
        od;
        csq = true;
        assert (!(csp && csq));
        csq = false;
        wantq = false;
        turn = 1
    od
}

선형 시간 논리란 논리의 기초 위에서 시간의 개념을 더한 것이다. []는 영원히 1임을 의미하고, <>는 미래에 결국 1이 나타날 것을 의미한다.
http://web.iitd.ac.in/~sumeet/slide3.pdf
https://www.youtube.com/watch?v=KVQdTjvtyUw
dekker.pml의
ltl { []<>csp && []<>csq }
하다
영원히 반복 되풀이 p에 들어가는critical section & 영원히 반복 되풀이 q에 들어가는critical section
이 말은 starvation을 검사하는 데 사용됩니다. 만약 프로그램이 p를 반복해서 실행하고 q를 실행하지 않을 능력이 있다면, jspin은 오류를 보고할 것입니다.
ltl을 검사할 때acceptance 모드를 선택하십시오.
starvation 테스트할 때 weak fairness 빼기.
뜻은 반복적으로 실행할 수 있는 프로세스가 무한히 반복될 수 있도록 허용하고 매번 그가 실행하며 다른 프로세스가 실행되지 못하게 하는 것이다(현실적인 컴퓨터 cpu에서는 비현실적이다)
만약 당신의 프로그램에 starvation freedom이 있다면 상술한 상황은 영원히 나타나지 않을 것이다