Formalising the Interface between Software and Hardware

This document is an extract from research proposal CMS1277 submitted to Science Foundation Ireland for funding. What is the question that this proposal addresses? Verifying the cor-rectness of safety-critical computer systems, particularly those that control ma-chinery and vehicles, is an important but complex task. Many disparate aspects of the system need to modelled, each with their own peculiarities and interac-tions. This is why one of the Grand Challenges in Computer Science, GC6, on “Dependable Systems Evolution ” [JOHW06] focusses on techniques to mathe-matically 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 in-dustrially inspired case-studies: recent such studies have included, for example