A Simplification of a Real-Time Verification Problem

Details A Simplification of a Real-Time Verification Problem A Simplification of a Real-Time Verification Problem

2010-08-08

arxiv.org/abs/1008.1417v1

Proc. of Automated Technology for Verification and Analysis (ATVA'07), LNCS 4762, pp. 284-299, 2007

Computer Science

Logic in Computer Science

32 Pages, 6 Figures. A preliminary version of this draft appeared in the proceedings of ATVA 2007

Scientific paper

10.1007/978-3-540-75596-8_21

We revisit the problem of real-time verification with dense dynamics using timeout and calendar based models and simplify this to a finite state verification problem. To overcome the complexity of verification of real-time systems with dense dynamics, Dutertre and Sorea, proposed timeout and calender based transition systems to model the behavior of real-time systems and verified safety properties using k-induction in association with bounded model checking. In this work, we introduce a specification formalism for these models in terms of Timeout Transition Diagrams and capture their behavior in terms of semantics of Timed Transition Systems. Further, we discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of (a large fragment of) these timeout and calender based transition systems into that on clockless finite state models through a two-step process comprising of digitization and canonical finitary reduction. This technique enables us to verify safety invariants for real-time systems using finite state model-checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction based proof methodology. Moreover, we can verify liveness properties for real-time systems, which is not possible by using induction with infinite state model checkers. We present examples of Fischer's Protocol, Train-Gate Controller, and TTA start-up algorithm to illustrate how such an approach can be efficiently used for verifying safety, liveness, and timeliness properties specified in LTL using finite state model checkers like SAL-smc and Spin. We also demonstrate how advanced modeling concepts like inter-process scheduling, priorities, interrupts, urgent and committed location can be specified as extensions of the proposed specification formalism.

Affiliated with

Also associated with

No associations

Rating

A Simplification of a Real-Time Verification Problem does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Simplification of a Real-Time Verification Problem, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Simplification of a Real-Time Verification Problem will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-313429