Title :
Modeling and verification of distributed real-time systems based on CafeOBJ
Author :
Ogata, Kazuhiro ; Futatsugi, Kokichi
Author_Institution :
Graduate Sch. of Inf. Sci., JAIST, Ishikawa, Japan
Abstract :
CafeOBJ is a wide spectrum formal specification language based on multiple logical foundations: mainly initial and hidden algebra. A wide range of systems can be specified in CafeOBJ thanks to its multiple logical foundations. However, distributed real-time systems happen to be excluded from targets of CafeOBJ. The authors propose a method of modeling and verifying such systems based on CafeOBJ, together with timed evolution of UNITY computational models.
Keywords :
algebraic specification; distributed algorithms; program verification; real-time systems; specification languages; CafeOBJ; UNITY computational models; algebraic specification; distributed real-time systems; distributed real-time systems modeling; hidden algebra; initial algebra; multiple logical foundations; timed evolution; wide spectrum formal specification language; Aerospace control; Algebra; Computational modeling; Distributed computing; Formal specifications; Information science; Patient monitoring; Protocols; Real time systems; Timing;
Conference_Titel :
Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on
Print_ISBN :
0-7695-1426-X
DOI :
10.1109/ASE.2001.989804
