Art

J-GLOBAL ID：202002247556816520   Reference number：20A1192528

Specification and verification of real-time multitasking systems by the OTS/CafeOBJ method

OTS/CafeOBJ法によるマルチタスク実時間システムの形式的検証

Author (4)： HIGASHI SHUKI (富山県大) ,  NAKAMURA MASAKI (富山県大) ,  SAKAKIBARA KAZUTOSHI (富山県大) ,  OGATA KAZUHIRO (北陸先端科学技術大学院大)
Material： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
Volume： 119  Issue： 470(MSS2019 57-68)  Page： 25-30  Publication year： Mar. 02, 2020 
JST Material Number： S0532B  ISSN： 0913-5685  Document type： Proceedings
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： computer processing system ,  system ,  real time processing ,  *verification ,  formal description ,  transition system ,  specification ,  *specification language ,  constraint condition (restriction) ,  mutual exclusion ,  equational logic ,  formal specification description ,  time constraint
Semi thesaurus term： multitask ,  real time system ,  formal verification ,  algebraic specification ,  specification language ,  mutual exclusion ,  system verification

JST classification (1)： Other fundamental theory of information engineering  (JB06000C)

Reference (15)：

• P. C. Ölveczky and J. Meseguer, Semantics and Pragmatics of Real-Time Maude, Higher-Order and Symbolic Computation, Springer, 20, 1-2, pp.161-196, 2007.
• Johan BengtssonWang Yi, Timed Automata: Semantics, Algorithms and Tools, Lectures on Concurrency and Petri Nets: Advances in Petri Nets, number 3098 in LNCS, pp.87-124, 2004.
• Kim Guldstrand Larsen and Paul Pettersson and Wang Yi, UPPAAL in a Nutshell, International Journal of Software Tools for Technology Transfer, Vol.1, No.1-2, pp.134-152, 1997.
• R. Diaconescu and K. Futatsugi, CafeOBJ Report, World Scientific, Singapore, 1998.
• 二木厚吉,緒方和博,中村正樹, CafeOBJ入門(1)-(6), コンピュータソフトウェア, 25(2) pp.1-27, 25(3) pp.69-80, 25(4) pp.68-84, 26(1) pp.71-83, 26(2) pp.93-106, 2008, 2009.

Terms in the title (4)： OTS ,  マルチタスク ,  実時間システム ,  形式的検証