High Integrity Hardware-Software Codesign

Between March 1998 and April 2004 I researched and wrote a Ph.D. thesis at the Open University, examining the use of programmable logic devices (PLDs) in high-integrity systems. The chapters of the thesis were:

1. Introduction, description of the general problems of high-integrity systems.
2. Literature survey, examining the areas of safety-critical systems and standards, programmable logic devices, applications of PLDs, and issues in the use of PLDs in critical systems.
3. Derivation and statement of the problems that the thesis aims to address, with criteria for assessing the completeness of solutions.
4. Examination and extension of the technologies key to the thesis: Synchronous Receptive Process Theory (SRPT) process algebra, the Pebble PLD programming language and the SPARK high-integrity subset of Ada.
5. Definition and use of a formal refinement system for SRPT, including complete derivation of a carry look-ahead adder.
6. Specification and design of an example interpreter of SPARK Ada based on a PLD, designed using SRPT.
7. Case studies of implementing the Chapter 5 carry look-ahead adder in Pebble and simulating it, and the implementation of a missile guidance system in SPARK with a critical section transformed into a SPARK Ada implementation.
8. Summary of the thesis, audit against the Chapter 3 problem statements, and conclusions.

Resources available on this web site:

Thesis (1.1Mb PDF)

The final version of my Ph.D. thesis, formatted as per the copy submitted to the British Library. 271 single-space pages.

Publications

A list of my publications to date, which give the reader a staged tour of the thesis.

Missile test harness (tarred gzip)

Ada source for the missile guidance system and simulator as described in Chapter 7 of the thesis.

Pebble simulator (tarred gzip)

Perl source for the Pebble simulator of PLD programming as described in Chapter 7 of the thesis.