ＣａｆｅＯＢＪ入門（１）形式手法とＣａｆｅＯＢＪ
書誌事項
- タイトル別名
-
- Introducing CafeOBJ (1) : Formal Methods and CafeOBJ
抄録
CafeOBJ言語システムを用いた形式手法，すなわち形式仕様の作成法と検証法，を全6回にわたり解説する．CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり，振舞仕様，書換仕様，パラメータ化仕様などが記述できる最先端の形式仕様言語である．CafeOBJ言語システムは，等式を書換規則として実行することで等式推論を健全にシミュレートすることができ，対話型検証システムとして利用出来る．<BR>第1回の今回は，「待ち行列を用いる相互排除プロトコル」を例題として，言語や検証法の細部に立ち入ることなく，CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する．第2回以降では，言語の構文と意味(第2回)，等式推論と項書換システム(第3回)について説明し，証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する．さらに，認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する．
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 25 (2), 1-13, 2008
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390282679715378176
-
- NII論文ID
- 130004549105
-
- ISSN
- 02896540
-
- 本文言語コード
- ja
-
- データソース種別
-
- JaLC
- CiNii Articles
-
- 抄録ライセンスフラグ
- 使用不可