Formal Methods for Developing High Assurance Computer Systems: Working Group Report

摘要

The Second International Workshop on Industrial- Strength Formal Techniques (WIFT'98) was held in October, 1998, in Boca Raton, Florida. At the workshop, four different discussion groups investigated various topics. This report summarizes the discussions conducted on the topic 'Formal Methods for Developing High Assurance Systems.' High assurance computer systems are computer systems where convincing evidence is required that the system satisfies a collection of critical properties. To operate correctly, these systems must satisfy properties such as safety and security. Examples of high assurance systems include flight control systems, medical systems, and control systems for nuclear plants. In addition, increased reliance on communications is moving many communications systems, such as telephone networks and cellular and satellite communications systems, into the domain of high assurance systems. The aim of the 1998 discussion was to revisit and continue a discussion began in the working group with the same name at the first WIFT in 1995. A report describing the discussions at WIFT'95 is available at the web site: http://www.cse.msu.edu/WIFT98/.