Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-540-75596-8_21 | Clinical Orthopaedics and Related Research |
Keywords | Field | DocType |
finite state veri- cation,timeout and calendar model,real-time systems,clockless model,process scheduling,real time systems,state space,model checking,real time | Model checking,Computer science,Algorithm,Theoretical computer science,Timeout,Finitary,Invariant (mathematics),Formalism (philosophy),State space,Bounded function,Liveness | Journal |
Volume | ISSN | Citations |
abs/1008.1 | Proc. of Automated Technology for Verification and Analysis
(ATVA'07), LNCS 4762, pp. 284-299, 2007 | 1 |
PageRank | References | Authors |
0.37 | 18 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Indranil Saha | 1 | 296 | 18.27 |
| Janardan Misra | 2 | 165 | 14.33 |
| Suman Roy | 3 | 21 | 7.25 |