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

fYear

2001

fDate

26-29 Nov. 2001

Firstpage

185

Lastpage

192

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-1426-X

Type

conf

DOI

10.1109/ASE.2001.989804

Filename

989804