Developing High Assurance Systems: On the Role of Software Tools

摘要

Recently, researchers have developed a number of powerful, formally based software tools, such as model checkers and theorem provers. To date, these tools have largely been used to analyze hardware designs. In the future, they should have significant value for analyzing the requirements and designs of software systems, especially high assurance software systems, where compelling evidence is needed that the system satisfies critical properties, such as safety and security properties. This paper briefly describes the different roles that formally based software tools can play in debugging, verifying, and testing software systems and software system artifacts. It also describes one important activity in software development not involving tools that is often neglected and that merits greater care and attention.