An Industrial Application of Model Checking to a Vessel Control System
Type of content
Conference Contributions - Published
UC permalink
Publisher's DOI/URI
Thesis discipline
Degree name
Publisher
University of Canterbury. Electrical and Computer Engineering
Journal Title
Journal ISSN
Volume Title
Language
Date
2011
Authors
Keating, D.M.
McInnes, A.I.
Hayes, M.P.
Abstract
Model checking allows an abstracted finite state 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.
Description
Citation
Keating, D.M., McInnes, A.I., Hayes, M.P. (2011) An Industrial Application of Model Checking to a Vessel Control System. Queenstown, New Zealand: IEEE 6th International Symposium on Electronic Design, Test and Application (DELTA 2011), 17-19 Jan 2011.
Keywords
model checking, SPIN, TTCAN, vehicle control
Ngā upoko tukutuku/Māori subject headings
ANZSRC fields of research
Field of Research::09 - Engineering::0906 - Electrical and Electronic Engineering