文献

J-GLOBAL ID：200902286316209842   整理番号：09A0026797

状態遷移表に基づくモデル検査の支援環境

Model Checking Support Environment based on State Transition Matrix

著者 (1件)： 小池隆 (富士ソフト)
資料名： 情報処理学会研究報告  (IPSJ SIG Technical Reports)
巻： 2008  号： 116(EMB-10)  ページ： 91-96  発行年： 2008年11月20日 
JST資料番号： Z0031B  ISSN： 0919-6072  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： モデル検査はソフトウェアの設計品質向上に有効な技術だが,モデル記述言語と時相論理を習得して検査モデルと制約条件を記述しなければならないことが,産業界への普及の妨げとなっている。そこで,状態遷移表と付加的な表から制約条件まで含む検査モデルを自動生成するモデル検査支援環境を作成し,複数の組込みソフトウェア開発プロジェクトへの適用によって評価した。(著者抄録)

シソーラス用語： *モデル検査 ,  *状態遷移図 ,  *ソフトウェア設計 ,  品質保証 ,  時間論理 ,  制約条件 ,  生産 ,  ソフトウェア ,  プロジェクト ,  システム評価 ,  自動生成 ,  組込みソフトウェア ,  品質評価
準シソーラス用語： モデル記述言語 ,  時相論理 ,  *状態遷移表

分類 (2件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R)

引用文献 (3件)：

• 渡辺政彦. 拡張階層化状態遷移表設計手法Ver. 2.0-Embedded SEのための設計手法. 1998
• HOLZMANN, G. J. The Spin Model Checker : Primer and Reference Manual. 2003
• 中島震. SPINモデル検査-検証モデリング技法. 2008

タイトルに関連する用語 (3件)： 状態遷移表 ,  モデル検査 ,  支援環境