Abstract
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 describe real-time systems and verify their properties. Concretely, we evolve UNITY computational models by introducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing system in CafeOBJ and verify that the system has a safety property based on the specification with the help of the CafeOBJ system.