PROPOSAL OF HYBRID VERIFICATION METHOD IN ASYNCHRONOUS REAL-TIME SOFTWARE INCLUDING TIMING CONSTRAINTS SPECIFICATION

A verification system of asynchronous real-time software including tim ing constraints, which supports both model-checking algorithms and lan guage inclusion algorithms, does not exist. In a language inclusion al gorithm, verification specification is described by a timed automaton from the standpoint of both states and behaviors. On the other hand, i n a model-checking algorithm, verification specification is described by real-time temporal logic from the standpoint of state relation. It is necessary to specify verification property by both timed automaton and real-time temporal logic. A hybrid verification method, which supp orts both verification methods, is proposed here. In order to realize it, a timed Kripke structure is generated from timed automaton through an augmented region graph. The method is shown to be effective using the example of a clock problem.