Paper Info
Title
A Framework For Specification And Verification Of Timeout Models Of Real-Time Systems
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-22606-9_18
CONTEMPORARY COMPUTING
Keywords
Field
DocType
Timeout models, Timeout Transition Diagram, Graphical Specification, GraphML, SAL
Asynchronous communication,Functional verification,Programming language,Pattern recognition,Graphical language,ANSI C,Computer science,Timeout,Symbolic data analysis,Artificial intelligence,Formalism (philosophy),Semantics
Conference
Volume
ISSN
Citations 
168
1865-0929
0
PageRank 
References 
Authors
0.34
10
1
Name
Order
Citations
PageRank
Janardan Misra116514.33