Model Checking is Possible to Verify Large-scale Vehicle Distributed Application Systems
Haitao Zhang1, Ayang Tuo1 and Guoqiang Li2
1School of Information Science and Engineering, Lanzhou University, China
2School of Software, Shanghai Jiao Tong University, China
ABSTRACT
OSEK/VDX is a specification for vehicle-mounted systems. Currently, the specification has been widely adopted by many automotive companies to develop a distributed vehicle application system. However, the ever increasing complexity of the developed distributed application system has created a challenge for exhaustively ensuring its reliability. Model checking as an exhaustive technique has been applied to verify OSEK/VDX distributed application systems to discover subtle errors. Unfortunately, it faces a poor scalability for practical systems because the verification models derived from such systems are highly complex. This paper presents an efficient approach that addresses this problem by reducing the complexity of the verification model such that model checking can easily complete the verification.
