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

fYear

2011

fDate

17-19 Jan. 2011

Firstpage

83

Lastpage

88

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Electronic Design, Test and Application (DELTA), 2011 Sixth IEEE International Symposium on

Conference_Location

Queenstown

Print_ISBN

978-1-4244-9357-9

Type

conf

DOI

10.1109/DELTA.2011.24

Filename

5729545