Formal Verification of Timed Transition Models
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.