Object-oriented method for real-time systems based on timed automaton

It is useful to introduce object-orientation into an analysis and design methodology for real-time systems. We have proposed such an object-oriented methodology for real-time systems, which is integrated with a timed automaton, but, using the proposed method, the verification cost is very large. In this paper, we focus on the verification of a dynamic model and propose two effective verification methods as follows. (1) In the explicit enumeration method, we represent state transitions as list structures. (2) In the implicit enumeration method, we represent state transitions as BDDs (binary decision diagrams). Using a depth-first search algorithm (in case 1) or inverse image computation (in case 2), we search for SCCs (strongly connected components) satisfying the acceptance conditions and test whether the SCCs are reachable from the initial states. At the same time, we check the timing constraints. We have developed an actual verification system and shown our method to be effective