Abstract
This chapter presents cha resents a study of the SAE J1708 Serial Communication link described in [1]. The study is carried out in Event-B, an extension of the B method. The system is implemented and decomposed using step-wise refinement. We p resent how to derive with this method a cycle-accurate hardware model. The model of the communication link system is composed of an arbitrary, itra finite, number of identical components that run concurrently. The model contains synchronization of these components required to control access to the communication link. At the end of the refinement we obtain an implementable model of the components which is translated into VHDL. The generated VHDL design is synthesizable, meaning that the implementable B model is synthesizable as well.
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
SAE International. SAE J1708 revised OCT93, serial data communication between microcomputer systems in heavy-duty vehicle, http://www.sae.org
Jean-Raymond Abrial. Event Driven Electronic Circuit Construction, August 2001
J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In B’98: Recent Advances in the development and Use of the B Method, volume 1393 of LNCS, 1998
Michael Leuschel and Michael Butler. ProB: A Model Checker for B. In FME 2003: Formal Methods, volume 2805 of LNC S, 2003
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
Zimmermann, Y., Hallerstede, S., Cansell, D. (2004). Formal Modelling of Electronic Circuits Using Event-B. 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_13
Download citation
DOI: https://doi.org/10.1007/978-1-4020-2867-0_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5256-1
Online ISBN: 978-1-4020-2867-0
eBook Packages: Springer Book Archive