Test design with model-based testing
Model-based testing sounds like the holy grail of quality assurance: efficiency, automation and maximum precision. But in practice, you stumble...
Formal methods are crucial for ensuring software correctness. They enable mathematical proofs of freedom from errors in safety-critical systems. The use of proof assistants and automated tools significantly increases the quality of software. These methods complement conventional tests and provide valuable insights into the reliability of software.
In the latest episode of the Software Testing Podcast, we celebrate World Quality Week. I talk to Lars and Bianca about how to mathematically prove freedom from defects in software and which tools can help. Bianca uses examples from the financial and automotive industries to explain why certain systems require absolute freedom from errors. Lars complements the conversation with insights into formal methods and how they are applied in practice. One particularly interesting topic was how AI can support us in providing evidence.
“I can’t prove freedom from errors with tests. There are simply certain domains where I need to be able to prove the absence of errors.” - Lars Hupel, Bianca Lutz
Lars Hupel is Chief Evangelist for Digital Currencies at Giesecke+Devrient, an international security technology company. As part of this role, Lars holds and writes numerous lectures, workshops and articles to make the technology behind digital currencies accessible to a broad audience. With a background as a software developer, Lars also contributes to product development and represents the company on various industry bodies. Lars holds a PhD in logic and verification from the Technical University of Munich and uses this knowledge to make Giesecke+Devrient’s products even more secure.
Bianca Lutz is a software architect at Active Group GmbH and works from Berlin. She was already interested in formal methods during her studies and worked with the proof assistant Isabelle/HOL. However, she is still fascinated by technical topics such as operating systems, especially embedded systems. She has been involved in various scientific publications, is a Linux kernel contributor and has published in Isabelle’s Archive of Formal Proofs as part of her thesis. After working in the insurance industry for several years, where she mainly dealt with legacy code, she switched to the functional programming camp in 2022.
In the field of software testing, absolute freedom from errors is difficult to guarantee. However, in certain industries - such as finance, automotive or medical technology - the requirements for freedom from errors are particularly high, as even small errors can have drastic consequences. For this reason, systems in such areas must be tested and validated with particular care.
Tests alone are often not enough to ensure complete correctness in safety-critical systems. Formal methods are used here and make it possible to provide mathematically rigorous proofs of the correctness of software. The use of proof assistants ensures that there are no logical gaps in the reasoning and checks. These methods complement conventional tests and increase the reliability of the results.
In practice, formal methods are often associated with considerable additional work. For example, it may be necessary to write up to ten lines of proof code for each line of regular code. Nevertheless, there are also less complex approaches such as type systems or model checkers, which are less comprehensive but still provide valuable insights and increase the quality of testing.
Automation and artificial intelligence (AI) are playing an increasingly important role in the creation of formal proofs. Some modern tools, such as Isabel, already use machine learning algorithms to generate proofs faster and significantly reduce manual effort. Such automated processes make the application of formal methods more efficient and accessible.
The combination of tests and formal methods is crucial to ensure the highest software quality. These techniques are not a stand-alone solution, but a valuable addition to traditional testing methods. Advances in the field of AI open up new opportunities to further develop these methods and make them even more widely applicable. The future therefore promises exciting developments in the interaction between AI and formal verification.
Formal methods are mathematically based approaches to the specification, development and verification of software and hardware systems. They use logic and mathematical models to prove the correctness and reliability of software and avoid errors during the development process.
Formal methods are important because they provide high accuracy and security by using mathematical proofs to avoid errors. They minimize the risk of errors in safety-critical systems and provide tighter control over the operation and integrity of software.
Frequently used formal methods are model checking, theorem proving and temporal logic. Model checking systematically checks all possible states of a system, while theorem proving uses mathematical proofs to confirm logical statements. Temporal logic examines correctness across time sequences.
Model Checking automatically tests all possible states of a system to find errors and is suitable for smaller, finite systems. Theorem Proving, on the other hand, proves mathematical theorems to confirm certain properties and is suitable for more general, but often more complex systems.
The application of formal methods can be challenging as it requires a lot of mathematical expertise and high computing power. In addition, the tools are often complex and time-consuming, which limits their applicability to large, complex systems.
Model checking is a formal method that systematically checks the state spaces of a system to ensure that there are no unexpected or undesired states. It is often used in safety-critical systems where all possible scenarios need to be checked.
Formal methods are particularly suitable for safety and mission-critical systems, such as in aerospace, medical technology, the automotive industry and nuclear technology. They are also used when software has to meet very high reliability requirements.
Temporal logics are logical systems that make it possible to analyze temporal sequences and states of a system. They are often used in model checking to ensure that states are fulfilled at certain times and thus confirm the correctness of the temporal behavior.
There are several software tools that support formal methods, including SPIN for model checking, Isabelle and Coq for theorem proving and TLA+ for the specification and verification of complex systems. These tools provide tools for modeling, checking and proof.
Formal methods could play a greater role in the future, especially in areas that require absolute reliability. Although their application is currently limited by high effort and complexity, improvements in tools and hardware could make their use increasingly practicable.
Model-based testing sounds like the holy grail of quality assurance: efficiency, automation and maximum precision. But in practice, you stumble...
Gamification describes a playful way of working together. And it can also be implemented in software development and testing. The field is broad:...
Test data plays a central role in modern software development. It enables data errors to be identified at an early stage and quality assurance to be...