프로멜라

PROMELA(Process or Protocol Meta Language)는 Gerard J. Holzmann에 의해 소개된 검증 모델링 언어이다. 이 언어는 분산 시스템과 같은 병행(concurrent) 프로세스를 모델링하기 위해 동적 생성을 허용한다. PROMELA 모델에서, 메시지 채널을 통한 통신은 동기식 (즉, 랑데부(rendezvous))) 또는 비동기식 (즉, 버퍼링(buffered))으로 정의(define)될 수 있다. PROMELA 모델은 모델링된 시스템이 원하는 동작을 수행하는지 확인하기 위해 SPIN 모델 검사기로 분석될 수 있다. Isabelle/HOL을 통해 검증된 구현은 "오토마타의 컴퓨터를 이용한 검증" 프로젝트의 일부로도 이용 가능하다. 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
키워드
다음 식별자는 키워드 사용을 위해 예약되어 있다.

 각주 

분류:명세 언어