HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

Formal modelling of electronic circuits using event-B, Case Study: SAE J1708 Serial Communication Link

Yann Zimmermann 1 Stefan Hallerstede Dominique Cansell 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Electronic systems become more and more complex and they are now involved in a lot of products. Malfunction of an electronic circuit may have financial consequences or take a heavy tool in human life. Formal methods are needed to ensure correctness of systems. This chapter presents a study of the SAE J1708 Serial Communication link described in. 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 present how to derive with this method a cycle-accurate hardware model. The model of the communication link system is composed of an arbitrary, 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.
keyword : systèmes proof systems refinement formal modelling raffinement modélisation formelle preuve
Document type :
Book sections
Complete list of metadata
https://hal.inria.fr/inria-00100144
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:14:39 AM
Last modification on : Friday, February 4, 2022 - 3:30:54 AM

Identifiers

  • HAL Id : inria-00100144, version 1

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE | INRIA2

Citation

Yann Zimmermann, Stefan Hallerstede, Dominique Cansell. Formal modelling of electronic circuits using event-B, Case Study: SAE J1708 Serial Communication Link. Jean Mermet. UML-B - Specification for Proven Embedded Systems Design, Kluwer Academic Publishers, 2004. ⟨inria-00100144⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

504

 

Contact                    Legal Notice                    Personal Data