Title :
Controller area network: a formal case study
Author :
Benzekri, Abdelmalek ; Bruel, Jean-Michel
Author_Institution :
Lab. IRIT/SIERA, Toulouse, France
Abstract :
We present a formal analysis of a Controller Area Network (CAN) controller using the Z specification language. It is a step in the evaluation of functional and performance properties of CAN applications. We first show how an external view of CAN controller functionalities can be held in Z. Z is based on set theory and first order logic and is very expressive: a unique notation allows the specification of data structures and operations. An internal view as also given and analyzed. Validation of the CAN controller specification is done and a property is shown; we demonstrate that this specification implements the satisfaction of the highest priority message being transmitted first
Keywords :
formal logic; formal specification; industrial control; peripheral interfaces; specification languages; CAN applications; CAN controller; CAN controller functionalities; CAN controller specification; Z specification language; controller area network controller; data structures; first order logic; highest priority message; performance properties; set theory; Communication industry; Communication system control; Communications technology; Computer aided software engineering; Control systems; Data structures; Distributed computing; Logic; Set theory; Specification languages;
Conference_Titel :
Factory Communication Systems, 1997. Proceedings. 1997 IEEE International Workshop on
Conference_Location :
Barcelona
Print_ISBN :
0-7803-4182-1
DOI :
10.1109/WFCS.1997.634321
