The research goal is to build a specification and analysis methodology for safety-critical software. Although past research included techniques to enhance safety throughout the software development process, the recognition that most accidents can be traced back to inadequate requirements and design foresight has led to concentration on the early parts the software life cycle. This work will build an integrated set of software requirements and design methods and techniques to increase confidence in the safety of software requirements and design methods and techniques to increase confidence in the safety of software that is controlling critical systems such as aircraft and other transportation systems, medical devices, and nuclear power plants. It will lead to better understanding what is required to provide a "safety analyst's workbench" that would allow software and systems engineers to build models and perform a variety of analyses on the software requirements and design in order to predict and verify a wide range of software properties during development. The above goals will be pursued within the context of a real, safety- critical avionics (Collision Avoidance of TCAS) system in order to provide a testbed to validate practicality, effectiveness, and feasibility as the hypotheses and ideas are generated and to keep the research on a track toward realistic and usable results. The testbed approach will allow evaluation of alternatives in a realistic setting, altering directions when necessary, and validating and demonstrating results on a real system.
