Promela
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2017/07/14 08:42 UTC 版)
「SPINモデルチェッカ」の記事における「Promela」の解説
その名前(Process Meta Language)が示すように、元来通信プロトコルの検証のために設計された言語である。検査対象であるシステムは非同期並行動作するプロセスの集まりとして記述される。C言語に似た文法を持ち、各プロセスの振る舞いを手続き的に記述する。プロセス間通信、非決定的な振る舞いを明示的に記述する文法要素を備えている。 コード内にアサーションをおくことができる。線形時相論理で記述される検証項目はモデル全体に関する性質を記述するのに対して、アサーションはそれが置かれた場所で満たすべき条件を記述する。
※この「Promela」の解説は、「SPINモデルチェッカ」の解説の一部です。
「Promela」を含む「SPINモデルチェッカ」の記事については、「SPINモデルチェッカ」の概要を参照ください。
ウィキペディア小見出し辞書の「Promela」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- Promelaのページへのリンク
