프로멜라
(Promela에서 넘어옴)
PROMELA(Process or Protocol Meta Language)는 Gerard J. Holzmann에 의해 소개된 검증 모델링 언어이다. 이 언어는 분산 시스템과 같은 병행(concurrent) 프로세스를 모델링하기 위해 동적 생성을 허용한다. PROMELA 모델에서, 메시지 채널을 통한 통신은 동기식 (즉, 랑데부(rendezvous))) 또는 비동기식 (즉, 버퍼링(buffered))으로 정의(define)될 수 있다. PROMELA 모델은 모델링된 시스템이 원하는 동작을 수행하는지 확인하기 위해 SPIN 모델 검사기로 분석될 수 있다. Isabelle/HOL을 통해 검증된 구현은 "오토마타의 컴퓨터를 이용한 검증" 프로젝트의 일부로도 이용 가능하다.[1] Promela로 작성된 파일은 일반적으로 .pml 파일 확장자를 가진다.
언어 참조[편집]
자료형[편집]
| 이름 | 크기(비트) | 이용 | 범위 |
|---|---|---|---|
| bit | 1 | unsigned | 0..1 |
| bool | 1 | unsigned | 0..1 |
| byte | 8 | unsigned | 0..255 |
| mtype | 8 | unsigned | 0..255 |
| short | 16 | signed | −215..215 − 1 |
| int | 32 | signed | –231..231 − 1 |
키워드[편집]
다음 식별자는 키워드 사용을 위해 예약되어 있다.
- active
- assert
- atomic
- bit
- bool
- break
- byte
- chan
- d_step
- D_proctype
- do
- else
- empty
- enabled
- fi
- full
- goto
- hidden
- if
- inline
- init
- int
- len
- mtype
- empty
- never
- nfull
- od
- of
- pc_value
- printf
- priority
- prototype
- provided
- run
- short
- skip
- timeout
- typedef
- unless
- unsigned
- xr
- xs