Formal Verification of Timed Transition Models

Hong Zhang


Labeled Transition Systems (LTSs) are used to express specifications and implementations of software. State-Event Labeled Transition Systems (SELTS's) extend LTS's by adding a state output map and an event map. A Timed Transition Model (TTM) is a timed extension of SELTS. The extension involves lower and upper time bound constraints and transitions, that relate to the number of occurrences of the special transition tick. A TTM can be described as a SELTS with a timer attached to each different transition, so that we can specify the time requirements of the model. This thesis gives the definitions of invariants, strong equivalence and weak equivalence for SELTSs and TTMs in PVS. It also provides a unified modeling environment for SELTSs and TTMs in PVS which allows the user to specify them easily. Further, the thesis illustrates the use of the modeling environment in PVS to prove invariants, weak equivalence and strong equivalence of SELTS s and TTM s by providing one example in each category. Finally we use our modeling environment to fomalise and verify the correctness on an industrial real-time controller.

Our method has the advantage that is simplifies the procedure for translating SELTS and TTMs into PVS. A disadvantage is that it still needs a number of interactions between the user and PVS, although some of theses could be considered as routine work.