Automated Modeling of Real-Time Implementation

Peter Krogsgaard Jensen

December 1998


This paper describes ongoing work on the automatic construction of formal models from Real-Time implementations. The model construction is based on measurements of the timed behavior of the threads of an implementation, their causal interaction patterns and external visible events. A specification of the timed behavior is modeled in timed automata and checked against the generated model in order to validate their timed behavior

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.