Towards a combination of CafeOBJ and PAT

In the quest for tractable formal methods to improve the practice of software engineering, both CafeOBJ [7] and PAT [12] have made great achievements based on different formal techniques. CafeOBJ has an evident advantage in specifying concurrent systems with object-oriented methods and proving behavioral properties based on reusability of proof. However, it is difficult to be applied to automatically verify some LTL based properties which involve complex state updates and finite path of states. Conversely, PAT offers great flexibility to simulate system behaviors and support modeling checking various properties, but it is difficult to prove behavioral properties directly, the definition of which is based on the structure of contexts. In the paper, we attempt to combine the two approaches by modeling specifications and verifying properties in CafeOBJ and PAT. A keyless car system is provided to illustrate our approach.