Testing Formal Semantics: Handel-C - Corcoran, Brian (Trinity College Dublin. Department of Computer Science, 2005)
This dissertation addresses the formal semantics of Handel-C: a C-based language with true parallelism and priority-based channel communication, which can be compiled to hardware. It describes an implementation in the Haskell functional programming language of a denotational semantics for Handel-C, as described in (Butterfield & Woodcock, 2005a). In particular, the Typed Assertion Trace trace model is used, and difficulties in creating a concrete implementation of the abstract model are discussed. An existing toolset supporting a operational semantics for the language is renovated, in part to support arbitrary semantic ?modes,? and to add support for the denotational semantics using this feature. A comparison module is written to compare the traces of two programs in any semantic mode supported by the simulator. Random testing support is implemented via the QuickCheck testing tool for Haskell. This tool is incorporated into the comparison module, allowing testing of various properties of Handel-C, as well as its traditional use of testing the Haskell implementation for errors. This support is used to search for discrepancies between the operational and denotational semantic models. Finally, several proposed ?Laws of Handel-C? are implemented and tested using the QuickCheck module. Some errors in the specification of the laws are discovered and corrected. Once the specifications are corrected, all of the proposed laws pass, paving the way for future formal verification.
Keywords: Computer Science