Specifying and verifying a railroad crossing with cafeOBJ
Kazuhiro Ogata, Kokichi Futatsugi · 2005
CafeOBJ is a wide spectrum specification language based on multiple logical foundations. CafeOBJ can be used to specify dynamic as well as static aspects of systems including object-oriented and reactive systems and verify their properties with the help of the CafeOBJ system. In this paper, we show that CafeOBJ can be also used to de-scribe real-time systems and verify their properties. Con-cretely, we evolve UNITY computational models by intro-ducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing sys-tem in CafeOBJ and verify that the system has a safety prop-erty based on the specification with the help of the CafeOBJ system. 1.