EN 
DE Practical application of formal methods
Authors: Christine Jakobs, Matthias Werner; Chemnitz University of Technology
Contribution – Embedded Software Engineering Congress 2018
The traditional development process for software in the field of embedded real-time systems assumes a static system with fixed components. Market demand is driving a need for greater dynamism. This increases complexity and makes it more important to ensure the preservation of safety-critical properties through rigorous modeling and analysis.
Embedded systems have become indispensable in our daily lives. Driver assistance systems and intelligent factory controls are examples of how highly specialized computer systems permeate our lives. To meet these demands, these systems must usually perform their tasks in real time. They often interact directly with their environment and therefore must meet high safety standards.
Development of software for embedded systems
As in many industrial sectors, embedded systems software is typically programmed by domain experts. These experts must transfer their specialized knowledge and apply it to the programming, usually using low-level programming languages. Embedded system software must meet stringent requirements. Compared to software for general-purpose computers, the non-functional properties are more complex, and the process for verifying them is governed by numerous standards.
The classic development process for software in embedded systems therefore usually starts with a static system. The software components and the configuration of the overall system are defined during the development process and analyzed with regard to their functional and non-functional properties. This analysis typically assumes the system's maximum configuration, for example, the comfort version in a vehicle. This maximum system is then analyzed to ensure it meets safety requirements. If the analysis is positive, it is assumed that every other system will also meet these requirements. The problem is that this static software architecture does not allow for future modifications. Therefore, the system must be completely reconfigured whenever an update is needed. On the other hand, analyzing the system in its maximum configuration also leads to another problem: hardly any purchased system is ever delivered with this configuration. Consequently, the system is built based on a constant overestimation of its capabilities.
Dynamic embedded systems
In addition to the problems described above in the classic development process for embedded systems, a paradigm shift is currently underway, driven by technological advancements and the associated expectations and demands of customers. For example, the automotive industry is increasingly using software to offer driver assistance systems. The networking between vehicles and their environment opens up a new attack vector for these safety-critical systems. As a result, software updates for bug fixes are becoming the norm. It is no longer sufficient to update the vehicle during service visits. Instead, it is becoming necessary to be able to update vehicles "over-the-air" at any time. Furthermore, there is a growing trend to move away from using custom-built hardware in embedded systems and towards "commercial-off-the-shelf" hardware. This opens up the possibility of placing software on the hardware via high integration. However, this flexibility in configuration through updates and high integration comes at the cost of increased complexity, which, among other things, makes it more difficult to verify non-functional properties. Because this complexity makes proof through simple testing increasingly difficult, it is necessary to resort to modeling and analysis of these dynamically composed systems.
Modeling and analysis of embedded systems
Based on industry standards, such as ISO 26262 for the automotive sector, modeling and analysis methods for embedded systems can be divided into three groups:
- Informal methods: Syntax and semantics are not fully defined, e.g., diagrams, images.
- Semi-formal methods: The syntax is fully defined, but the semantics are incompletely defined, e.g., UML.
- Formal methods: Syntax and semantics are fully defined, e.g., Z-notation, TLA+
The automotive industry defines four different levels (ASIL AD) that describe the criticality of a component. In the case of highly integrated software, the software component with the highest level determines the verification methods for all components if the system's lack of feedback cannot be proven.
The methods that can be used to verify non-functional properties are diverse, and apart from informal methods, they can be used for all safety levels. Informal and semi-formal modeling methods are considered simpler and therefore cheaper to use. At first glance, this seems to be the case, as they require little training. However, in practice, several modeling and analysis methods are usually employed to support the various stages of the development process. This requires considerable effort to translate the different models. Nevertheless, this often leads to unwieldy models that partially overlap, resulting in a loss of overview of the overall process. The required dynamics further increase the complexity, which the currently used modeling methods do not support, or do not support to the necessary extent.
Temporal logic as a cross-tool meta-language
While the classic use case for formal methods is the specification and subsequent verification of a system or individual components, we propose a holistic approach in which classical verification methods are specifically applied to model-based development. Specifically, we use TLA, a temporal logic.
Temporal logics belong to the modal logics. Statements in these logics are only valid under certain conditions/in certain modes. Within these modes, the familiar propositional logic applies, while globally the extensionality principle does not hold.
Temporal logics make statements about the temporal order of statements without relying on a specific underlying time model. Instead, they make statements such as "it is always true that…", "at some point it is true that…", or "it is true… until… is true." This facilitates the analysis of systems with different time models (e.g., distributed systems).
TLA, or rather its specification language TLA+, is already successfully used in industry. Lamport developed TLA to support both modular development processes and the composition of different time models. To achieve this, TLA allows the model to "stutter." This means that there are steps in which the system variables under consideration do not change. As a result, when composing models, a link between the process descriptions can be omitted. Instead, the models can be analyzed competitively, since while one model stutters, another has the opportunity to generate progress.
The specification of system components with TLA+ enables their analysis with regard to their functional and non-functional properties. For this purpose, TLA+ offers the possibility to directly verify criteria such as liveness and reachability.
If the rules of system composition are also specified using TLA+, a subsequent analysis allows the generation of a software architecture that complies with these rules and thus with the required non-functional properties of the architecture. For example, the corresponding configurations for the operating system can be generated from the real-time critical software components by specifying the scheduling criteria.
This holistic approach enables its application throughout the entire development process. This is based on the targeted support of modularization and composition in the specification language. As a result, it allows for flexible switching between the levels of model-based development.
Application examples from Google and Amazon demonstrate the suitability of TLA+ as a specification language for both small software components and large distributed systems. Our own examples show that this "turning the specification language on its head" for generating architectures yields the desired results using simple means. By using PlusCal as the algorithm language for TLA+, the composition operators used can be easily specified, directly translated into TLA+, and analyzed using a C-like syntax.
Summary and Outlook
The world of safety-critical embedded systems is currently undergoing a transformation. Assumptions of a static system are becoming obsolete due to the demand for simple software updates. This increases the complexity of developing software for embedded systems and demonstrating their functional and non-functional properties.
Temporal logics, specifically TLA+, enable a holistic approach to specifying and analyzing such systems throughout the entire development process. Both individual software components and composition operators can be modeled. This allows the software architecture to be generated generatively, inherently guaranteeing the required non-functional properties.
authors
Christine Jakobs She studied business administration and computer science and has been researching cyber-physical systems since her master's thesis. She is particularly interested in properties such as real-time capability and reliability. Her doctoral research aims to use formal methods to ensure that future safety-critical systems, especially in the transportation sector, remain manageable even under the demands of today's market for flexibility.
Prof. Matthias Werner He studied electrical engineering and control engineering at Humboldt University of Berlin, where he also earned his doctorate. After research stays in Austin and Cambridge (UK), he completed his habilitation at the Technical University of Berlin, focusing on the properties of reliable systems. He holds the professorship for operating systems at the Technical University of Chemnitz. His research interests include the design and analysis of runtime systems, taking into account properties such as real-time capability, mobility, and reliability.
Download the article as a PDF file
Real-time – MicroConsult Training & Coaching
Do you want to bring yourself up to date with the latest technology?
Then find out more here MircoConsult offers training courses/seminars/workshops and individual coaching on the topic of embedded and real-time software development.
Training & coaching on the other topics in our portfolio can be found here. here.
Real-time expertise
Valuable expertise in the field of embedded and real-time software development is available. here Available for you to download free of charge.
You can find expertise on other topics in our portfolio here. here.
