Bibliographic Metadata
Bibliographic Metadata
- TitleInduction-based Verification of Timed Systems : / vorgelegt von Tobias Isenberg, M.Sc.
- Author
- Participants
- Published
- EditionElektronische Ressource
- Description1 Online-Ressource (xvi, 203 Seiten) : Diagramme, Tabellen
- Institutional NoteUniversität Paderborn, Fakultät für Elektrotechnik, Informatik und Mathematik, Univ., Dissertation, 2016
- AnnotationTag der Verteidigung: 10.05.2016
- Defended on2016-05-10
- LanguageEnglish
- Document TypesDissertation (PhD)
- URN
Links
- Social MediaShare
- Reference
- IIIF
Files
Classification
Zusammenfassung
Die korrekte Funktionalität rechnergesteuerter Systeme ist von großer Wichtigkeit, da diese Systeme oftmals in sicherheitskritischen Szenarios eingesetzt werden. Viele dieser Systeme besitzen zeitgesteuertes Verhalten. Um die Qualität der Systeme sicherzustellen, können Modell-basierte Design-Ansätze verwendet werden in denen die zu erstellenden Systeme mithilfe von Modellen entworfen werden. Die Nutzung formaler Methoden kann die Abwesenheit von fehlerhaftem Verhalten sicherstellen. In dieser Arbeit werden Netzwerke von zeitlichen Automaten betrachtet. Die Analyse dieser Modelle ist schwierig, insbesondere bei der Exploration großer, komplexer Modelle. Zusätzlich gehen bestehende Analyseverfahren nicht effizient mit Änderungen am Model um. In dieser Arbeit wird eine Technik zur Verifikation von Sicherheitseigenschaften, die die Abwesenheit von fehlerhaftem Verhalten definieren, vorgestellt. Diese Technik hat ein grundlegend anderes Funktionsprinzip als andere Ansätze, da sie Induktion nutzt und versucht die explizite Exploration und Speicherung von Zuständen zu vermeiden. Hierdurch ist sie eine wertvolle Ergänzung zu den bestehenden Ansätzen. Bei Änderungen am Modell werden die errechneten induktiven Invarianten des Ansatzes wiederverwendet. Dies funktioniert sehr gut bei einer speziellen Art von Systemen, genannt Parametrisierte Zeitliche Systeme, in der der Parameter die Anzahl der zeitlichen Automaten vorgibt. Die Technik erlaubt die Verifikation der gesamten Familie an Modellen, unabhängig von der Anzahl an Automaten. Hierzu wird die Sicherheitseigenschaft für die kleineren Modelle verifiziert und danach verwendet, um über die gesamte Familie an Modellen zu urteilen. Zusätzlich wird untersucht, wie man die induktiven Invarianten für allgemeine Änderungen und Modelle nutzen kann.
Abstract
Computer controlled systems are a foundation to today's society. Correctness of the functionality provided by these systems is of importance, since they are often deployed in safety-critical scenarios. Many of these systems include timed behavior. In order to ensure the quality of these systems, model-based design approaches can be employed where the systems under development are designed using models. The absence of erroneous behavior in these models can be ensured with formal methods. In this work, we use the modeling formalism of networks of timed automata. We approach two deficiencies of analysis techniques for these models. First, they easily run out of memory when exploring large, complex models. Second, they do not handle changes of the models efficiently. We provide a technique for the verification of safety properties specifying the absence of erroneous behavior for networks of timed automata. Our technique deliberately works distinct from other approaches in this field, as it employs induction and avoids explicit exploration and storage of states. In consequence, it is a valuable complement to existing technologies. Furthermore, in the presence of reconfigurations (i.e., changes) we reuse inductive invariants computed by our algorithm. This idea works well for a special class of systems, denoted Parameterized Timed Systems, where the number of timed automata is given as parameter. Our technique enables a verification of the entire system, irrespective of the actual number of automata. To this end, we verify the safety property for the smaller models of the family and reuse the computed inductive invariants to reason about the larger models. In addition, we examine the reusability of the inductive invariant for general models and reconfigurations.
Content
Stats
- The PDF-Document has been downloaded 55 times.
License/Rightsstatement
