16th IEEE International Conference on Automated Software Engineering (ASE'01)
Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ
San Diego, California
November 26-November 29
ISBN: 0-7695-1426-X
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. In this paper, we propose a method of modeling and verifying such systems based on CafeOBJ, together with timed evolution of UNITY computational models.
Index Terms:
algebraic specification, CafeOBJ, distributed real-time systems, modeling, specification, UNITY, verification
Citation:
Kazuhiro Ogata, Kokichi Futatsugi, "Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ," ase, pp.185, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001