Formalising the Interface between Software and Hardware (FISH)

Funded by Science Foundation Ireland .
Start Date: September 2008, 3 yrs.

Verifying the correctness of safety-critical computer systems, particularly those that control machinery and vehicles, is an important but complex task. Many disparate aspects of the system need to modelled, each with their own peculiarities and interactions. This is why one of the Grand Challenges in Computer Science, GC6, on "Dependable Systems Evolution" focusses on techniques to mathematically verify the correctness of such systems. The goal of GC6 is to develop a repository of verified software components, consisting of formal specifications and software implementations along with proofs of correctness supported by automated proof tools and proof assistants.

GC6 is a long-term research programme with a time horizon of ten to fifteen years. At present it is engaged in a series of research activities based around industrially inspired case-studies: recent such studies have included, for example, the validation of the Mondex smart-card's security protocols. A more recent case-study that has been adopted is that of a verified file-store for use in mission critical applications, suggested by NASA researchers who need such high-dependability systems for space research missions.

This project builds on initial work on the formal modelling of flash memory systems, to use this case-study within GC6 to develop a comprehensive theoretical foundation for reasoning about hardware systems and their interface to software.

This is viewed as being complementary to the notion of ``hardware/software co-Design'', that focusses on techniques for partitioning a system specification into hardware and software components in an efficient manner.

This project is being run in collaboration with Professor Jim Woodcock at the University of York.

More details about the project are in a Research Programme Summary document (PDF).