|
Technical Report HW-MACS-TR-0037
Title | Verifying Temporal Properties in HW-Hume |
---|
Authors | Gudmund Grov, Andrew Ireland, Greg Michaelson, Kevin Hammond (St. Andrews) |
---|
Date | 2006-02-08 |
---|
Abstract | HUME is a modern formally-defined programming language targeted at safety-critical, resource-bounded systems. A key feature of HUME is the clear separation between computation and coordination, achieved through a finite-state-automata based approach, where a purely functional computation layer is embedded into a reactive coordination layer that manages interactions between processes and with the external state. It is our contention that this design makes formal analysis more tractable than for more conventional programming languages, such as C and Java, and hardware description languages, like VHDL and Verilog, since the formal proof requirements for each layer can be cleanly separated. In particular, coordination properties may be established directly without the need for explicit abstraction away from underlying control structures. This
paper describes the use of model checking to verify the correctness
of HUME software systems at the coordination layer. A specification
language which captures correctness and temporal properties
is created for HUME and is exploited through application of the SPIN
model checker. This approach to verifying Hume coordination has
been successfully applied to a range of examples. |
---|
Group | Dependable Systems |
---|
Notes | |
---|
Download | |
---|
|
|