Art

J-GLOBAL ID：200902298161424049   Reference number：09A1196855

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

Author (1)： OGATA KAZUHIRO (北陸先端科学技術大学院大)
Material： 計測と制御  (Journal of the Society of Instrument and Control Engineers)
Volume： 48  Issue： 11  Page： 816-821  Publication year： Nov. 10, 2009 
JST Material Number： F0131A  ISSN： 0453-4662  CODEN： KESEA  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *security system ,  *verification ,  *specification description ,  theorem proving ,  Time ,  dynamic system ,  model checking ,  *formal specification description
Semi thesaurus term： CafeOBJ ,  RT Maude ,  real time ,  *security system ,  *formal verification ,  dynamic system

JST classification (1)： Logic algebra  (JB03000H)

Reference (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)

Terms in the title (6)： 安心 ,  システム構築 ,  形式検証 ,  代数仕様 ,  実時間システム ,  検証