Controller area network: a formal case study

Author

Benzekri, Abdelmalek ; Bruel, Jean-Michel

Author_Institution

Lab. IRIT/SIERA, Toulouse, France

fYear

1997

fDate

1-3 Oct 1997

Firstpage

365

Lastpage

372

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Factory Communication Systems, 1997. Proceedings. 1997 IEEE International Workshop on

Conference_Location

Barcelona

Print_ISBN

0-7803-4182-1

Type

conf

DOI

10.1109/WFCS.1997.634321

Filename

634321