COMPASS '94 featured two full-day tutorials and two half-day tutorials. In the first full-day tutorial, John McDermid (University of York) and Christopher Locke (York Software Engineering Limited) discussed the general characteristics of formal methods, formal methods in Z, and a tool, Computer Aided Design in Z (CADiZ). Hans-Ludwig Hausen (German National Research Center for Computer Science) gave the second full-day tutorial on "Software System Evaluation and Certification." This tutorial focused on methods and tools for the evaluation and assessment of software products and processes. The first half-day tutorial, on "Software Hazard Analysis," was given by Nancy Leveson (University of Washington). Software hazard analysis techniques were described in the context of a system engineering approach. Marvin Schaefer (Arca Systems, Inc.) conducted the final, half-day tutorial on "Trusted DBMS Considerations and Issues. The conference opened with welcoming remarks by H.O. Lubbes and Jan Filsinger, COMPASS '94 General Co-Chairs, and John McLean, COMPASS '94 Program Chair. A tools fair was introduced at this conference. Fifteen tools were exhibited by nine vendors: Risk Watch (Expert Systems Software, Inc.); AeSOP and ARiES (The Aerospace Corporation); EVES (ORA; Ottawa); AdaWise, Penelope, Romulus, and Larch-Ada (ORA; Ithaca), McCabe Toolset (McCabe & Associates); ModeChart Toolset (NRL); Centurion (SRS Technologies); RDD-100 (Ascent Logic Corporation); Boundary Flow Covert Channel Analysis (CTA, Inc.); INTERLOCKS (CSA); and FDR Tool.
The Keynote address was delivered by Admiral (Retired) Jerry O. Tuttle. Admiral Tuttle presented the importance of computer systems in the present day world. This dependence on critical systems demands that the systems are built with safety and security assurances. He noted the explosion in information and the ever increasing need to build secure systems, not just in military systems but in industry as well. He said, "opportunity is often disguised as unsolvable problems." He concluded that we should accept this challenge to improve technology to make systems safe and secure.
Conference sessions were devoted to "Safety," "Use and Assessment of Formal Methods,", "Alternatives to Formal Verification," "Fault Tolerance," "Concurrency and Real-Time Systems," "Hardware Verification," and "Security." Papers presented at the first Safety session described applications in the Lockheed C-130J Software Requirements, of fault tree analysis using Petri nets, and of hazard analysis. The second session devoted to Safety contained papers treating the evaluation of software for nuclear power plants, risk analysis in the software requirements phase, and the use of formal methods for the development of software requirements in safety-critical systems.
Three papers were presented in the session "Use and Assessment of Formal Methods." The design of Ada 9x, a case study applying formal methods to the system specification of a safety-critical system, and the efficacy of formal methods in dependability assessment comprised this session.
Alternatives to formal verification presented in the next session consisted of an extension to a specification-based testing method and the application of an informal program verification method to the inspection of Ada source code. The "Fault Tolerance" session consisted of three papers. The first described a computer-aided software fault tolerance design and analysis tool. The second presented a method for estimating "coverage probabilities." The last paper in this session summarized a fault model and its application to an asymmetric architecture.
Two papers in the session "Concurrency and Real-Time Systems" discussed methods to reduce the number of states in a state-space model, one applying to Ada tasking. The last paper in this session presented a methodology for preventing the specification of physically impossible and contradictory systems. Two papers were presented in the Hardware Verification session, one presenting an approach to formalizing VHDL and the other describing experiences in verifying a network component.
The "Security" session contained a paper proposing a method of reducing the threat of covert channels without crippling performance. The two remaining papers discussed experience with security, the last using college students to break into a computer system.
A panel session was devoted to "Software Testability for Critical Systems." Panel members consisted of Jeff Voas (Reliable Software Technologies Corporation), Dick Hamlet (Portland State University), William E. Howden (University of California), and Keith Miller (Sangamon State University). W.E. Howden's presented views on testability, failure rates, detectability, trustability and reliability.
Jeff Voas talked about testability, testing and critical software assessment. Complexity measures and coverage criteria are only two classes of measures in the class of testability metrics. Software testability is a metric that analyzes the code itself in a "white-box" fashion. A testability measurement plan will decrease development costs and will not in any way slow down progress.
In Dick Hamlet's absence, Keith Miller presented Dick Hamlet's views on software reliability. He discussed software reliability that is inherently dependent on the very nature of software. One cannot measure software reliability with efforts made in development. Instead, we ought to seek the relationship between defect-detection methods employed during the development and the quality of these methods.
Keith W. Miller discussed testability, including its theoretical aspects, its practical implementation, and its application to reliability estimation. He described the complementary advantages and disadvantages of random testing and testability analysis. Finally, he talked about how a fully automated system, PISCES, makes testability analysis possible without any oracle for correctness.
The COMPASS '94 banquet speaker, Professor Brian Randell of the University of Newcastle upon Tyne, summed up COMPASS this way:
"COMPASS is filling a need that no other conference is attempting. COMPASS recognizes that problems in security may be shared by software safety and system safety, and vice versa. In both cases, reliability is the goal to be achieved. COMPASS looks at formal proofs, testing, and fault tolerance methods as complementary instead of rival approaches. Most of all, COMPASS is bringing together software and hardware communities, security and safety communities from industry, government and academia. Together, these communities may make great gains in solving the problems of providing computer assurance in complex systems, such as aerospace systems, medical devices, military weapons, and transportation.
COMPASS '95 will be held 26-30 June 1995, at NIST in Gaithersburg, Maryland. The deadline for papers submitted for COMPASS '95 is 14 January 1995. For information about COMPASS '95 or on obtaining proceedings of COMPASS '94, contact:
Dolores Wallace
Computer Systems Laboratory
National Institute of Standards and Technology
Bldg. 225, Room B266
Gaithersburg, MD 20899-0001
(301) 975-3340, Fax: (301) 926-3696,
[email protected]
