Specification and Verification of Real-Time Systems Using the OTS/CafeOBJ Method: A Tutorial

Nakamura, Masaki

doi:10.51094/jxiv.3874

##article.authors##

Nakamura, Masaki Toyama Prefectural University https://researchmap.jp/masaki-n

DOI:

https://doi.org/10.51094/jxiv.3874

キーワード:

CafeOBJ、 Observational transition system、 Real-time system、 Hybrid system、 Fischer's mutual exclusion protocol、 Autonomous vehicle group control

抄録

This paper presents a tutorial on specification and verification of multitask real-time systems using the OTS/CafeOBJ method, in which systems are modeled as observational transition systems (OTSs) and their specifications are described in CafeOBJ, an algebraic specification language.
One important feature is that systems with an arbitrary number of processes can be handled and verified by the proof score method.
In this tutorial, we describe how the OTS/CafeOBJ method can be extended to model multitask real-time systems.
As case studies, we model Fischer's mutual exclusion protocol and an autonomous vehicle group control system. For each example, we show how the system is specified in CafeOBJ and how safety properties are verified by proof scores.

利益相反に関する開示

なし

ダウンロード *前日までの集計結果を表示します

ダウンロード実績データは、公開の翌日以降に作成されます。

引用文献

R. Diaconescu and K. Futatsugi, CafeOBJ Report, World Scientific, Singapore, 1998.

A. Riesco, K. Ogata, M. Nakamura, D. Gaina, D.D. Tran, and K. Futatsugi, Proof Scores: A Survey. ACM Comput. Surv. 57, 10, Article 251, 37 pages, 2025.

K. Ogata, and K. Futatsugi, Proof scores in the OTS/CafeOBJ method, In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp.170-184, 2003.

K. Ogata and K. Futatsugi, Some tips on writing proof scores in the OTS/CafeOBJ method, In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol. 4060, pp.596-615, 2006.

K. Ogata and K. Futatsugi, Modeling and verification of real-time systems based on equations, Science of Computer Programming, 66(2), pp.162-180, 2007.

M. Nakamura, S. Higashi, K. Sakakibara, K. Ogata, Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Volume E105.A, Issue.5, pp.823-832, 2022.

Y. Wang, M. Nakamura, R. Takano, T. Matsumoto, K. Sakakibara, Multitask Hybrid Observational Transition System and its Application, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Volume E109.A, Issue 3, pp.638-650, 2026.

M. Fischer, Re: where are you? Electronic mail message from Michael Fischer to Leslie Lamport, Arpanet message sent on June 25, 1985 18:56:29 EDT, number 8506252257.AA07636@yale-bulldog.yale.arpa (47 lines), 1985.

L. Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, 5(1), pp.1-11, 1987.

E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, Springer, Vol.10, pp.1047-1110, 2018.