Formal Modelling of Electronic Circuits Using Event-B

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.