A Framework for Specification and Verification of Timeout Models of Real-Time Systems

Timeout based models are an important class of design models for discrete event modeling and simulation of real-time systems and protocols. In this work, we define a framework to graphically represent timeout based models with synchronous communication. The formalism offers system designers an expressive graphical language with well defined semantics to model their system designs and reason about their behavior. For actual implementation, these models are expressed using GraphML standard with support for embedded ANSI C code. We further devise an automated translation technique (and develop corresponding prototype tool support) to translate the GraphML designs into SAL (Symbolic Analysis Laboratory) model specifications, which in turn, can be formally verified using the SAL verification engine.