Loading…
Formal verification of model refactorings for hybrid control systems
Schlesinger, Sebastian
The ever growing complexity in modern embedded systems require to incorporate increasingly many functions into a single system. Such increasing functionality leads to growing design complexity. Model Driven Engineering (MDE) has been proposed to improve the complexity management for development of embedded systems. An industrially widely used technique to reduce the complexity of models and establish compliance with industrial MDE guidelines are refactorings. However, refactorings are often performed manually and may introduce erroneous behaviour. This may be critical especially in safety-critical environments. Thus, techniques to formally establish behavioural equivalence of source and target model of a refactoring are highly desirable. The main challenge for defining an approach for formal verification of behavioural equivalence of embedded systems is that these systems typically are hybrid control systems in the sense that they comprise both time-discrete and time-continuous behaviour. As a consequence, the data flow-oriented languages that are used to model such systems inherently have an approximate nature. This means that even though two models may be equivalent if interpreted in an ideal mathematical domain, their evaluation by a semantics of a data flow-oriented language may yield different values due to numerical approximations.
In this thesis, we present an approach for the semi-automatic formal verification of behavioural equivalence of hybrid control systems modelled in data flow-oriented languages. Our approach is formally well-founded, addresses the approximate nature of data flow-oriented languages, is automatable, and scales comparatively well for many industrially relevant applications. Our major contribution is twofold:
Firstly, we provide a sound methodology for the formal verification of behavioural equivalence of hybrid control models on data flow-oriented languages. Secondly, we largely automate our methodology for a subset of such models. We select Simulink as major representative of industrially relevant data flow-oriented languages. Our theoretical methodology is based on a formal operational semantics for Simulink, which we have adopted and extended to fit our needs. Based on the operational semantics, we define a novel denotational semantics, our so-called Abstract Representation, which describes an idealised behaviour of Simulink in terms of differential and difference equations. We show the soundness of our Abstract Representation with respect to the operational semantics. Then, we enable the formal verification of behavioural equivalence of semantical refactorings. An example for such a semantical refactoring is the replacement of an explicitly modelled differential equation by its analytical solution. To address the approximate nature of data flow-oriented languages, we adapt the equivalence notion of approximate bisimulation to Simulink. States are approximately bisimilar with a precision ε ≥ 0 if the distance of their values is at most ε. We provide sufficient conditions to conclude approximate bisimulation for two given models executed in the same finite simulation intervalI, and we provide means to calculate the precision ε(#I), which depends on the length of the simulation interval. Note that this differs from the usual application of approximate bisimulation in the literature. There, approximate bisimulation is applied to transition systems with infinite runtimes, i.e., the precision ε holds for arbitrary lengths of execution intervals.
We have largely automated our approach for the subset of models expressible as linear differential or difference equations. Via Laplace transform and z-transform, we are able to provide an almost fully automated, modular verification approach that uses a Computer Algebra System to perform the equivalence checks and calculations.We have implemented our automation approach and demonstrated its performance with experimental results.
Die wachsende Komplexität moderner eingebetteter Systeme erfordert es, immer mehr Funktionalität in die Systeme zu implementieren. Solch wachsende Funktionalität führt zu wachsender Komplexität im Design. Modellgetriebene Entwicklung (MDE) ist ein Mittel, um das Management der Komplexität zu verbessern. Eine industriell weit verbreitete Technik zur Reduktion der Modellkomplexität und zur Herstellung der Konformität der Modelle mit industriellen MDE Richtlinien sind Refactorings. Refactorings werden jedoch oft manuell durchgeführt und können daher oft fehlerhaft sein. Dies kann kritisch sein, insbesondere in sicherheitskritischen Umgebungen. Techniken, die es erlauben, die Verhaltensäquivalenz von Quell- und Zielmodell von Refactorings formal zu verifizieren sind daher wünschenswert.
Eine besondere Herausforderung bei der Definition einer Methodik für die formale Verifikation von Verhaltensäquivalenz für eingebettete Systeme ist, dass diese Systeme typischerweise hybride Kontrollsysteme sind, d.h. sie beinhalten zeit-diskretes und zeit-kontinuierliches Verhalten. Aus diesem Grunde weisen datenflussorientierte Sprachen, die zur Modellierung solcher Systeme verwendet werden, eine approximative Natur auf. Damit ist gemeint, dass obwohl zwei Modelle, interpretiert in einer idealisierten, mathematischen Weise, äquivalent sein mögen, es vorkommen kann, dass die Auswertung dieser Modelle durch eine Semantik einer datenflussorientierten Sprache zu abweichenden Werten durch numerische Approximationen führt.
In dieser Dissertation präsentieren wir einen Ansatz für die semi-automatische formale Verifikation der Verhaltensäquivalenz von hybriden Kontrollsystemen, die in einer datenflussorientierten Sprache modelliert sind. Unser Ansatz ist formal fundiert, berücksichtigt die approximative Natur der datenflussorientierten Sprachen, ist automatisierbar und skaliert relativ gut für viele industriell relevante Anwendungen. Der Ansatz besteht aus zwei Hauptteilen. Zunächst definieren wir eine theoretische Methodik für die formale Verifikation der Verhaltensäquivalenz von hybriden Kontrollmodellen auf datenflussorientierten Sprachen. Danach automatisieren wir weitgehend die Methodik für eine Teilmenge dieser Modelle. Wir wählen Simulink als Hauptvertreter der industriell relevanten datenflussorientierten Sprachen. Unsere theoretische Methodik basiert auf einer formalen operationalen Semantik für Simulink, die wir angepasst und erweitert haben, um sie für unsere Zwecke nutzbar zu machen. Wir beginnen mit der Definition einer denotationellen Semantik, unserer sogenannten Abstract Representation, die ein idealisiertes Verhalten von Simulink mittels Differential- und Differenzengleichungen beschreibt.
Wir zeigen die Korrektheit unserer Abstract Representation in Bezug auf die operationale Semantik. Die Abstract Representation ermöglicht die Verifikation der Verhaltensäquivalenz bei semantischen Refactorings, z.B. der Ersetzung eines Modells, das durch eine Differentialgleichung repräsentiert wird durch ein Modell, das deren analytische Lösung repräsentiert. Um die approximative Natur der datenflussorientierten Sprachen zu berücksichtigen, passen wir den Äquivalenzbegriff der approximierten Bisimulation an Simulink an. Zustände sind approximativ bisimilar mit einer Präzision ε ≥ 0 wenn ihre Werte höchstens ε voneinander entfernt sind. Wir präsentieren anschließend hinreichende Bedingungen, um auf die approximierte Bisimulation für zwei gegebene Modelle, die im selben endlichen Simulationsintervall I ausgeführt werden, schließen zu können. Dies beinhaltet Methoden zur Berechnung der Präzision ε(#I), die von der Länge des Simulationsintervalls abhängt.
Beachten Sie, dass dies von der in der Literatur üblichen Anwendung der approximierten Bisimulation abweicht. In der Literatur wird approximierte Bisimulation üblicherweise auf Transitionssysteme mit unendlicher Laufzeit angewandt, d.h. die Präzision ε gilt für beliebig lange Zeiten der Ausführung. Wir haben unseren Ansatz für eine Teilmenge von Modellen, die als lineare Differential- oder Differenzengleichungen darstellbar sind, weitgehend automatisiert. Mit Hilfe der Laplace- und z-Transformation sind wir in der Lage, eine nahezu vollständig automatisierte, modulare Lösung zur Verifikation zu präsentieren. Sie verwendet ein Computer Algebra System für die Äquivalenzcheckes und zur Berechnung. Wir haben unseren automatisierungsansatz implementiert und dessen Leistung mit experimentellen Ergebnissen demonstriert.
