文献

J-GLOBAL ID：200902293649864151   整理番号：09A1196853

安心・安全システム構築のための形式検証技術 時間オートマトンによる実時間システムの形式的検証

著者 (1件)： 中田明夫 (広島市大 大学院情報科学研究科)
資料名： 計測と制御  (Journal of the Society of Instrument and Control Engineers)
巻： 48  号： 11  ページ： 803-809  発行年： 2009年11月10日 
JST資料番号： F0131A  ISSN： 0453-4662  CODEN： KESEA  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： コンピュータシステムは広範囲な分野で利用され,実時間システムでの高信頼性が求められている。その検証システムのモデルとして,時間オートマトンがよく用いられる。本稿では,実時間システムの形式的検証技術の一つである時間オートマトンのモデル検査技術を解説した。例題とツールを用いた検証の実例を交えて紹介した。すなわち,時間オートマトン(定義,動作意味,並列合成,記述例:踏み切り制御システム),モデル検査,検証例(踏み切り制御システムを例に,モデル検査による検証例を紹介),を説明した。

シソーラス用語： *セキュリティシステム ,  検証 ,  *オートマトン ,  時間 ,  合成 ,  並列アルゴリズム ,  モデル検査 ,  踏切
準シソーラス用語： *安全システム ,  形式検証 ,  *時間付きオートマトン ,  *実時間

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

引用文献 (5件)：

• CLARKE, E. M. Model Checking. 1999
• ALUR, R. A theory of timed automata. Theoretical Comput. Sci. 1994, 126, 183-235
• SIPSER, M. Introduction to the Theory of Computation. 1996, chapter 1
• MAGEE, J. Concurrency : State Models and Java Programs. 2006
• LARSEN, K. G. UPPAAL in a nutshell. Int. Journal of Software Tools for Technology Transfer. 1997, 1, 1-2, 134-152

タイトルに関連する用語 (6件)： 安心 ,  システム構築 ,  形式検証 ,  時間オートマトン ,  実時間システム ,  形式的検証