Tech Reports Home Contact
Technical Report Series
Actions
Submit Report
Browse Reports
Information
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0037


TitleVerifying Temporal Properties in HW-Hume
AuthorsGudmund Grov, Andrew Ireland, Greg Michaelson, Kevin Hammond (St. Andrews)
Date2006-02-08
AbstractHUME 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.
GroupDependable Systems
Notes
Download

 

Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer