Abstract
We present a framework, which combines model checking and theorem prover based refinement for real-time systems design focusing on the refinement of non deterministic to timed deterministic finite state machines. Our verification flow starts from a cycle accurate finite state machine for the RAVEN model checker. We present a translation, which transforms the model into efficient B language code. After refining the RAVEN model and annotating it, the time accurate model is also translated to B so that the B theorem prover can verify the refined model almost automatically. The approach is introduced by the example of a mobile phone echo cancellation unit.
The work described herein is funded by the IST Project PUSSEE
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.R. Abrial. The B-Book. Cambridge University Press, 1996.
R. Alur and T.A. Henzinger. Reactive Modules. In LICS’96, 1996.
S. Blom et al. μCRL: A Toolset for Analysing Algebraic Specifications. In Proc. of CAV’01, 2001.
S. Berezin. Model Checking and Theorem Proving: A Unified Framework. PhD thesis, Carnegie Mellon University, 2002.
R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Number 23 in Perspectives in Computing. Academic Press, 1988.
E.M. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Lecture Notes in Computer Science, 131, 1981.
E.M. Clarke and W. Heinle. Modular Translation of Statecharts to SMV. Technical Report, Carnegie Mellon University, 2000.
M.J. Gordon. Introduction to HOL. Cambridge University Press, Cambridge, 1993.
Z. Manna et al. STeP: The Stanford Temporal Prover. Technical Report, Stanford University, 1994.
L. Mikhailov and M. Butler. An Approach to Combining B and Alloy. In D. Bert et al., editors, ZB’2002, Grenoble, France, 2002.
I. Oliver. Experiences of Model Driven Architecture in Real-Time Embedded systems. In Proc. of FDL02, Marseille, France, 2002.
I. Oliver. Model Driven Embedded Systems. In J. Lilius et al., editors, Proc. of ACSD2003, Guimarães, Portugal, 2002.
J. Ruf. RAVEN: Real-Time Analyzing and Verification Environment. J.UCS, Springer, Heidelberg, 2001.
N. Shankar. Combining Theorem Proving and Model Checking Through Symbolic Analysis. In CONCUR 2000, 2000.
J. Zandin. Non-Operational, Temporal Specification Using the B Method-A Cruise Controller Case Study. Master’s Thesis, Chalmers University of Technology and Gothenburg University, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this chapter
Cite this chapter
Krupp, A., Mueller, W., Oliver, I. (2004). Combined Formal Refinement and Model Checking for Real-Time Systems Verification. In: Grimm, C. (eds) Languages for System Specification. Springer, Boston, MA. https://doi.org/10.1007/1-4020-7991-5_19
Download citation
DOI: https://doi.org/10.1007/1-4020-7991-5_19
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-7990-0
Online ISBN: 978-1-4020-7991-7
eBook Packages: Springer Book Archive