Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/DELTA.2011.24 | Electronic Design, Test and Application |
Keywords | Field | DocType |
model checking,control systems specialist,industrial application,model checker,abstracted finite state model,design specification,vessel control system,exhaustive state space search,correctness property,new zealand,software design,formal specification,finite state machines,spin,control systems,software engineering,control system,formal verification,protocols,testing,synchronization | Abstraction model checking,Model checking,Software design,Computer science,Correctness,Real-time computing,Formal specification,Finite-state machine,State space search,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4244-9357-9 | 1 | 0.35 |
References | Authors | |
2 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Keating | 1 | 1 | 0.35 |
| Allan I Mcinnes | 2 | 9 | 4.32 |
| Michael Hayes | 3 | 2 | 2.05 |