Many computer-based systems must be certified for properties such as safety or security before they may be deployed. The higher levels of certification should consider every contingency and malfunction that may arise among and between the system, its components, and its environment. These considerations involve human judgment (to pare the vast space of potentially relevant issues), technical analysis (to provide evidence for correct and appropriate behavior in all cases), and human judgment again (to evaluate the evidence produced).
I will sketch some conventional processes for certification and outline more recent approaches based on "safety cases." All aspects of these processes are hugely expensive, and I will suggest how the costs might be reduced by expanding and automating the technical analysis component (i.e., making the overall activity "more scientific"). I will also describe issues in attempting to make certification compositional.
Reception to follow in the second floor atrium, Siebel Center.
John Rushby received B.Sc. and Ph.D. degrees in computing science from the University of Newcastle upon Tyne in 1971 and 1977, respectively. He joined the Computer Science Laboratory of SRI International in 1983, and served as its director from 1986 to 1990; he currently manages its research program in formal methods and dependable systems. This group developed and supports the PVS theorem proving and verification system, the ICS decision procedures, and the SAL suite of model checking tools. Prior to joining SRI, he held academic positions at the Universities of Manchester and Newcastle upon Tyne in England. His research interests center on the use of formal methods for problems in the design and assurance of dependable systems.
Dr. Rushby is a member of the IEEE, the Association for Computing Machinery, the American Institute of Aeronautics and Astronautics, and the American Mathematical Society. He is a former associate editor for Communications of the ACM and for IEEE Transactions on Software Engineering, and a former member of the editorial board for the journal Formal Aspects of Computing. He is the author of the (now rather outdated) chapter on formal methods for the FAA Certification Handbook. See his home page for more information.