kirancodes.me
To Proof Maintenance & Beyond!

Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ

Kazuhiro Ogata, Kokichi Futatsugi

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.

BibTeX
@inproceedings{Ogata-Futatsugi:ASE01,
  author    = {Kazuhiro Ogata and
               Kokichi Futatsugi},
  title     = {Modeling and Verification of Distributed {Real-Time} Systems Based on {CafeOBJ}},
  booktitle = {ASE},
  pages     = {185--192},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers