DocumentCode
2575672
Title
Modelling MajorCAN with UPPAAL
Author
Bonet, Matias ; Donaire, Gabriel ; Proenza, Julián
Author_Institution
Univ. de les Illes Balears, Palma
fYear
2007
fDate
25-28 Sept. 2007
Firstpage
1404
Lastpage
1407
Abstract
The controller area network (CAN) protocol produces data inconsistencies in some scenarios. A previous work proposed a new protocol called MajorCAN which is a small modification to CAN. MajorCAN does not present the reported error scenarios thus ensuring data consistency. Although MajorCAN has been thoroughly simulated, no formal verification has been performed so far. In this paper we describe how we have modelled MajorCAN using a network of timed automata in Uppaal. This is the first step of its formal verification by means of model checking.
Keywords
automata theory; controller area networks; formal verification; MajorCAN; controller area network; formal verification; model checking; timed automata; Automata; Automatic control; Automation; Automotive applications; Cyclic redundancy check; Formal verification; Hardware; Industrial control; Protocols; Transmitters;
fLanguage
English
Publisher
ieee
Conference_Titel
Emerging Technologies and Factory Automation, 2007. ETFA. IEEE Conference on
Conference_Location
Patras
Print_ISBN
978-1-4244-0825-2
Electronic_ISBN
978-1-4244-0826-9
Type
conf
DOI
10.1109/EFTA.2007.4416948
Filename
4416948
Link To Document