프로멜라

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