For Safety-Critical Systems
In medicine, transportation (fully automated trains, aerospace) and in energy production (atomic power plants), software errors can have severe consequences, The use of formal methods can help to prevent such bugs in advance. While the reliability of simple machines can be determined by testing, evaluating the safety of software-controlled machines with complex behavior is very difficult. Here tests can only detect the existence of errors, but cannot prove the absence of errors. Errors in software components can occur at various times in the course of the development process, starting with inadequate requirements specification and on to errors in the design and implementation and integration errors. All these errors pose potential dangers for the operation of the system. This has led to various approaches to improving the reliability of software.
In our interview, Dr. Christine Natschläger explains why formal methods will rise in importance in the future and why they continue to play a marginal role.
Prof. Dr. Egon Börger & Dr. Christine Natschläger in discussion about formal methods.
What are formal methods?
For the development of safety-critical software hat, an approach has evolved that seeks to avoid errors from the start. In formal methods, the focus is on conceptualizing the software. Formal methods build on mathematical modeling and formal logic and are used to specify and to test the software. With formal methods you start with a mathematical model and apply logical analysis to predict the attributes of a system. You can determine whether a system specification is internally consistent, whether certain attributes can be guaranteed, and whether requirements were designed and implemented correctly. Furthermore, you can use the specification for simulation/animation, code generation, test generation and test evaluation.
In what domains are formal methods highly suited?
Event-B and ASMs (Abstract State Machines) are used to develop safety-critical systems (e.g., the commuter rail service RER in Paris, which runs fully automatically and has never experienced a failure) and highly distributed software systems. In a production line with a series of robots that use the same software, if one robot fails, then the other robots need to detect the failure and take over the tasks of the defective robot. Formal methods are suited for such complex applications. Other application examples include dialysis devices, heart pacemakers and airplane components. All these systems are representative of safety-critical, embedded systems. The first challenge that they pose is their modeling. The second challenge is the proof of their adherence to safety requirements and of their correct functioning regarding the physical behavior of the devices.
How does software development with formal methods differ from conventional methods?
Much of the time and effort within a project shifts: More care is invested in requirement analysis, specification and the rough design; this additional effort delivers a return on investment or is even overcompensated because significantly less specification and design errors need to be detected and corrected during implementation and time is saved the test phase. With suitable model-based methods, the model used for specification, validation and verification can also be reused to support implementation, test suite creation, documentation and finally maintenance.
What are the characteristics of software development with formal methods
- Developers must know the system better
The system developer who is assigned the task of specification is forced to give more thought to the system to be developed and must understand it in detail. The invested time is more than in conventional methods. Yet because this developer thinks more carefully about what needs to be implemented, the subsequent steps (design, implementation, integration) prove to be less experimental, cause less errors and save time.
Formal methods enable us to validate the system before its implementation via animation and simulation.
Verification tests whether the specification is internally consistent (free of contradiction), whether certain attributes (e.g., safety requirements) can be guaranteed, and whether the requirements have been correctly implemented.
- Human-to-human communication
A formal specification provides precise statements (free of ambiguity) about the required behavior. Formalization thus supports unambiguous communication among developers.
- Automatic code generation
Given a sufficient degree of detail, some (operational) formalisms enable automatic code generation from the requirements specification. However, the generated code generally needs to be improved.
Can formal methods avoid all software errors?
Of all the errors that emerge during commissioning and during operation, most of them and the most expensive ones can be traced to the requirements specification. Errors in implementation are fewer and often easier (cheaper) to correct. Specification errors can extend through the complete implementation and require extensive changes. The most severe errors result when the required behavior was not specified. This can be checked via validation in the first step. The second most serious errors result when the design does not fulfill the requirements.
Effort required for using formal methods
The effort required for using formal methods is relatively low in the requirements specification phase and the number of errors that can be found is relatively high. During implementation the use of formal methods requires more effort and the number of errors that can be detected is lower. However, depending on the cost of possible errors (errors in safety-critical systems can endanger life), the use of formal methods can make sense here too.
- A more recent example of the introduction of formal methods has been reported by Amazon Web Services and describes how software quality and productivity were improved. See: How Amazon Web Services Uses Formal Methods: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract
- Software Competence Center Hagenberg also served as co-organizer of ABZ 2016, the international conference where developers and users of the most important model-based formal methods meet: http://www.cdcc.faw.jku.at/ABZ2016/