Title :
An Industrial Application of Model Checking to a Vessel Control System
Author :
Keating, Daniel ; McInnes, Allan ; Hayes, Michael
Author_Institution :
Electr. & Comput. Eng., Univ. of Canterbury, Christchurch, New Zealand
Abstract :
Model checking allows an abstracted finite state model of a system to be developed and a set of mathematically defined correctness properties, based on the design specifications, to be defined. The model checker performs an exhaustive state space search of the model, checking the correctness properties hold at each step. This paper describes how model checking has been applied to find and correct problems in the software design of a distributed vessel control system currently under development at a control systems specialist in New Zealand.
Keywords :
control engineering computing; finite state machines; formal specification; formal verification; industrial control; search problems; software engineering; New Zealand; abstracted finite state model; correctness properties; distributed vessel control system; exhaustive state space search; model checking; software design; Control systems; Delay; Protocols; Safety; Synchronization; Testing;
Conference_Titel :
Electronic Design, Test and Application (DELTA), 2011 Sixth IEEE International Symposium on
Conference_Location :
Queenstown
Print_ISBN :
978-1-4244-9357-9
DOI :
10.1109/DELTA.2011.24
