Formal Analysis and Verification of Embedded Systems for Healthcare
Sarmen Keshishzadeh
Promotors: prof.dr.ir. J.F Groote (TU/e) and prof.dr. J.J.M. Hooman (RU and TNO-ESI)
Copromotor: dr.ir. A.J. Mooij (TNO-ESI)
Technische Universiteit Eindhoven
Date: 24 March 2016, 14:00
Thesis: PDF
Summary
High-tech systems are becoming increasingly reliant on correct functioning software components. The increasing complexity of these components and the desire to deliver innovative products in a short period of time have motivated the need for systematic approaches to software development.
Model-Driven Software Engineering (MDSE) addresses the mentioned challenges by promoting the use of abstract models as the key elements in the development process; transformations are used to generate software from models. In the context of MDSE, it is a common trend to use modeling languages that are tailored to specific domains. Such a language is called a Domain-Specific Language (DSL) and aims to address only a limited set of problems. The language abstracts from the characteristics shared between this specific set of problems and focuses on describing the variations between them.
State-of-the-art DSL techniques (e.g., defining the concrete or abstract syntax for a DSL, code generation, writing unit tests at the level of DSL models) have boosted the applicability of DSLs in industrial practice. However, for safety-critical systems, more advanced techniques are required to give a level of certainty in the correctness of the developed software.
In this thesis we propose a vision for extending state-of-the-art DSL techniques in order to increase the reliability of software developed in DSL approaches. The main contributions can be summarized as follows:
- DSL approaches typically rely on an implicit semantics in terms of a transformation to implementation code. Such an implicit semantics becomes increasingly problematic when multiple transformations are constructed from the DSL to various artifacts. We propose to have an explicit formalization of the semantics that assigns precise meanings to the language constructs. Moreover, we apply the semantics and use automated formal techniques based on equivalence checking and model-based testing to validate the correctness of the generated artifacts with respect to the formalized semantics. The use of such automated techniques is particularly useful in an industrial context when there is no time for constructing proofs of correctness for the transformations.
- Further investigation of transformations from DSLs to implementation code and analysis models revealed that validating transformations becomes more challenging when implementation details introduced by a specific transformation are also relevant for the notion of consistency between the transformations. We explicitly distinguish between the semantics of a language and the implementation details introduced by a transformation and propose to have separate formalizations for these two components. These formalizations are the basis of our approach for validating the consistency between the implementation code and analysis models generated from a DSL model. We define conformance relations between the generated artifacts and DSL models. Test cases are generated based on these formal relations to validate the consistency of the generated code and analysis models with respect to the semantics and implementation details.
- • In addition to validating the correctness and consistency of transformations, we also studied ways to validate the correctness of DSL models with respect to certain desired properties. Such validation can discover modeling mistakes in DSL specifications that would otherwise be cascaded to the generated artifacts through the transformations. We also propose to extend this validation with an automated debugging procedure to assist the user in identifying the cause for a violated property. The debugging procedure identifies a potential cause for each violated property and traces it back to the syntactic constructs of the DSL.
- Finally, we turn our attention to the problem of analyzing models that rely on real numbers. The fact that real numbers are infinite objects imposes a major challenge in this context. Hence, there is a need to develop rigorous numerical methods that support formal analysis on models that contain real numbers. Correctness of computations should be guaranteed by such methods. To this end, we have developed a top-down exact real arithmetic approach and investigate the way the required precision of a given expression influences the required precision of its sub-expressions. We apply this approach to approximate various algebraic (e.g., addition, multiplication) and transcendental (e.g., exponential function, natural logarithm) operations. Detailed algorithms and proofs of correctness are provided for the considered operations.