Abstract
We present the adaptive cruise controller case study for B modelling and the Abstract: We P data model checking by RAVEN. Individual translations of B operations, data types, and invariants to the RAVEN Input Language are presented by the example of the case study.
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.
Similar content being viewed by others
References
J.R. Abrial. The B-Book. Cambridge University Press, 1996.
A. Krupp, W. Mueller. Deliverable D4.3.1: Specification of Real-Time Properties.Report, IST — Project PUSSEE, December 2002.
A. Krupp, W. Mueller. Deliverable D4.3.2: Refinement and Verification of RealTime Properties. Technical Report, IST — Project PUSSEE, April 2003
J. Ruf. RAVEN: Real-Time Analyzing and Verificationp 2003 Y g Environment. J.UCS, Springer, Heidelberg, 2001.
P.J. Turner, M.A. Leuschel. ProB V1.06 User Manual. Declarative Systems Software Engineering, University of Southampton, UK, 2004.
J. Zandin. Non-Operational, Temporal Specification Using the B Method — Cruise Controller Case Study. Master’s Thesis, Chalmers University d A and Gothenburg University, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science+Business Media New York
About this chapter
Cite this chapter
Krupp, A., Lundkvist, O., Schattkowsky, T., Snook, C. (2004). The Adaptive Cruise Controller Case Study. In: Mermet, J. (eds) UML-B Specification for Proven Embedded Systems Design. Springer, Boston, MA. https://doi.org/10.1007/978-1-4020-2867-0_12
Download citation
DOI: https://doi.org/10.1007/978-1-4020-2867-0_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5256-1
Online ISBN: 978-1-4020-2867-0
eBook Packages: Springer Book Archive