文献

J-GLOBAL ID：200902298161424049   整理番号：09A1196855

安心・安全システム構築のための形式検証技術 代数仕様に基づく実時間システムの検証

著者 (1件)： 緒方和博 (北陸先端科学技術大学院大)
資料名： 計測と制御  (Journal of the Society of Instrument and Control Engineers)
巻： 48  号： 11  ページ： 816-821  発行年： 2009年11月10日 
JST資料番号： F0131A  ISSN： 0453-4662  CODEN： KESEA  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 安心・安全システム構築のためには,システムをプログラミング言語等で実装する前に,きちんと設計(仕様記述)したほうが良い。モデル検査や対話的定理証明は,それを支援する技術の一つである。本稿では簡単な例題を用いて,実時間システムのRT Maudeによるモデル検査とCafeOBJによる対話的定期証明について解説した。すなわち,セルを介したデータ送信,ADSプロトコルのモデル化,Real-Time Maudeによる検証(仕様記述,モデル検査),RT Maudeによる検証(仕様記述,対話的定理証明),について紹介した。

シソーラス用語： *セキュリティシステム ,  *検証 ,  *仕様記述 ,  定理証明 ,  時間 ,  動的系 ,  モデル検査
準シソーラス用語： CafeOBJ ,  RT Maude ,  リアルタイム ,  *安全システム ,  *形式検証 ,  *形式的仕様記述 ,  動的システム

分類 (1件)： 論理代数  (JB03000H)

引用文献 (9件)：

• 1) 緒方和博,中村正樹,二木厚吉:代数仕様,知識ベース 1編 ソフトウェア基礎,4節,電子情報通信学会 (出版予定)
• 2) M. Clavel, et al.: All About Maude - A High-Performance Logical Framework, LNCS, 4350, Springer (2007)
• 3) R. Diaconescu and K. Futatsugi: CafeOBJ report, AMAST Series in Computing, 6, World Scientific (1998)
• 4) J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi and J.-P. Jouannaud: Introducing OBJ, In J. Goguen and G. Malcolm(eds.), Software Engineering with OBJ, Kluwer (2000)
• 5) 緒方和博,中村正樹,二木厚吉:Maude:書換え論理に基づく計算機言語および処理系,コンピュータソフトウェア,25-2, 78/84 (2008)

タイトルに関連する用語 (6件)： 安心 ,  システム構築 ,  形式検証 ,  代数仕様 ,  実時間システム ,  検証