Formal Methods for Safety Critical System Specification

For safety critical systems, hardware is often preferred over software because it is easier to achieve safety goals in hardware alone and because hardware is considered more reliable than software. But as systems become more complex, software solutions will also be important. Here we demonstrate, using a simple example, that formal methods are a useful tool for developing software specifications for safety critical systems, since they reduce ambiguity in the design and can be proven consistent. Using formal methods for specifications will enable the development of dependable, high-performance, reliable hardware/software safety critical systems. The method we describe is the first step in our work to establish a hardware/software development process for safety critical systems.