| dc.description.abstract | 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. | en |
