Title :
Modelling MajorCAN with UPPAAL
Author :
Bonet, Matias ; Donaire, Gabriel ; Proenza, Julián
Author_Institution :
Univ. de les Illes Balears, Palma
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;
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
DOI :
10.1109/EFTA.2007.4416948
