Please use this identifier to cite or link to this item: doi:10.22028/D291-25960
Title: Hierarchic decision procedures for verification
Author(s): Jacobs, Swen
Language: English
Year of Publication: 2009
SWD key words: Verifikation
Automatisches Beweisverfahren
Komplexes System
Free key words: Verifikationsmethode
Theorieerweiterungen
Zugsteuerungssystem
verification
theory extensions
complex systems
local reasoning
automatic train controller
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: Information-handling systems are becoming ever more complex. They may be pure hardware or software systems, or complex systems of hardware and software that act in a real-world environment. Verification is a method to ensure that systems behave in the expected way, which is a necessity for safety-critical applications like automatic railway control. The size of such systems makes manual verification impossible. Therefore, we need automatic or computer-aided verification procedures. Automated reasoning is already widely used in the analysis and verification of systems. For a restricted class of systems, the resulting verification problems are inherently finite and can be solved efficiently. For complex systems, such finiteness cannot be expected. To express and prove properties of these systems, we need a formal language and reasoners that can deal with universal quantification, arithmetic expressions and unbounded data structures at the same time. Thus, in recent years there has been new interest in the handling of firstorder formulas modulo a given background theory. The problem is known to be undecidable in general, and research focuses mostly on methods that solve many problem instances quickly, but sacrifice completeness. We take a different approach and focus on instances of this problem that we can show to be decidable. In this way we can solve the resulting problems efficiently and guarantee termination. This work is based on research by Sofronie-Stokkermans on local theory extensions and on work by Ganzinger and Korovin on instantiation-based firstorder theorem proving. We extend the existing work on local theory extensions, giving new examples of axioms which satisfy a locality condition and using ideas from instantiation-based first-order theorem proving to make local reasoning more efficient. Furthermore, we show that local theory extensions allow us to decide certain verification problems for parameterized systems and develop increasingly complex system models of an automatic train controller on which we demonstrate how to use local reasoning to verify safety properties of such systems.
Informationsverarbeitende Systeme werden ständig komplexer. Dies können reine Hardware- oder Softwaresysteme sein, oder komplexe Systeme von Hardware und Software, die mit ihrer physikalischen Umgebung interagieren. Mittels Verifikation kann sichergestellt werden, dass ein System sich in der erwarteten Weise verhält. Bei sicherheitskritischen Systemen, z.B. automatischen Zugsteuerungssystemen, ist dies unumgänglich. Die Größe solcher Systeme macht es unmöglich, ihr Verhalten von Hand zu verifizieren. Deshalb benötigen wir automatische oder computergestützte Verifikationsmethoden. Bei der Analyse und Verifikation von Systemen ist automatisches Beweisen bereits weit verbreitet. Für eine eingeschränkte Klasse von Systemen sind die auftretenden Verifikationsprobleme von Natur aus endlich and können effizient gelöst werden. Für komplexe Systeme kann eine solche Endlichkeit nicht angenommen werden. Um Eigenschaften solcher Systeme ausdrücken und beweisen zu können, brauchen wir eine formale Sprache und Beweismethoden, die mit universeller Quantifizierung, arithmetischen Ausdrücken und unbeschränkten Datentypen gleichzeitig umgehen können. Deshalb gab es in den letzten Jahren ein neues Interesse an Methoden, die universell quantifizierte Probleme in solchen Hintergrundtheorien lösen können. Es ist bekannt, dass solche Probleme im Allgemeinen unentscheidbar sind, und die Forschung konzentriert sich auf Methoden, die unter Verzicht auf Vollständigkeit möglichst viele Probleme schnell lösen können. Wir verfolgen einen anderen Ansatz und konzentrieren uns auf Problemklassen, deren Entscheidbarkeit wir zeigen können. Dadurch können wir diese Probleme effizient lösen und gleichzeitig das Terminieren der Prozedur garantieren. Diese Arbeit basiert auf der Forschungsarbeit von Sofronie-Stokkermans an lokalen Theorieerweiterungen, sowie der Arbeit von Ganzinger und Korovin an instanziierungs-basierten Methoden zum Theorembeweisen in Prädikatenlogik erster Ordnung. Wir führen die Arbeit an lokalen Theorieerweiterungen fort, indem wir neue Beispiele von Axiomen geben, die eine Lokalitätseigenschaft erfüllen, und benutzen Ideen aus instanziierungs-basierten Methoden zum Theorembeweisen in Prädikatenlogik, um lokales Beweisen effizienter zu machen. Weiterhin zeigen wir, dass lokale Theorieerweiterungen es uns ermöglichen, bestimmte Verifikationsprobleme für parametrisierte Systeme zu entscheiden und entwickeln eine Reihe komplexer werdender Modelle eines automatischen Zugsteuerungssystems an denen wir demonstrieren, wie man mittels lokalen Beweisens Sicherheitseigenschaften solcher Systeme verifizieren kann.
Link to this record: urn:nbn:de:bsz:291-scidok-29478
hdl:20.500.11880/26016
http://dx.doi.org/10.22028/D291-25960
Advisor: Sofronie-Stokkermans, Viorica
Date of oral examination: 29-Jan-2010
Date of registration: 4-May-2010
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
Dissertation_1436_Jaco_Swen_2010.pdf1,06 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.