The application of semi-formal and formal techniques within the software life cycle of safety critical applications

by Fausto Giunchiglia (ITC/IRST & University of Trento)

Wednesday 2 Feb 2000, 16:00 → 16:15 Europe/Zurich

500/1-001 - Main Auditorium (CERN)

The goal of this talk is to provide a short survey of various techniques, which can be used within the software life cycle in the case of safety critical applications. Safety critical applications are applications whose cost or possible impact on human lives requires the development of software of very high quality and as free from bugs as possible. The talk will describe some of the experiences done in the past 4-5 years by the group of Trento. We will start by describing a small number of success stories of previous industrial projects. For each project we will briefly highlight the application area, the problem solved, the methodology and tools used. The second part will provide more details about the methodology and technology that we use: Software development and deployment. Some hints of UML might also be provided. Validation and verification. After a brief introduction, we will concentrate on the model checking technology. Time permitting, we will provide a short description of NUMV, a model checker (developed jointly with CMU) which now counts more than 50 installations world-wide. The third line of research will highlight the lines of research and technology development that we are currently pushing. About the speaker Fausto Giunchiglia is professor of Computer Science (Artificial Intelligence and Software Engineering) at the University of Trento. He also collaborates with ITC-IRST (automated reasoning systems divisione), where he was Division head till November 1999. He has a Degree in Electronic Engineering (1981) and a Doctorate (1987) (specialization in Computer Science) from the University of Genoa. He worked at Stanford University (Computer Science Dept., 1984-1987). He was a Research Fellow at the University of Edinburgh (Dept. of Artificial Intelligence, 1987-1988), and a (part time) Visiting Fellow at Stanford University (Computer Science Dept., 1990-1997).