Hierarchic decision procedures for verification
Swen Jacobs · Max Planck Digital Library · 2009
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 standig komplexer. Dies konnen 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 verhalt. Bei sicherheitskritischen Systemen, z.B. automatischen Zugsteuerungssystemen, ist dies unumganglich. Die Grose solcher Systeme macht es unmoglich, ihr Verhalten von Hand zu verifizieren. Deshalb benotigen wir automatische oder computergestutzte Verifikationsmethoden. Bei der Analyse und Verifikation von Systemen ist automatisches Beweisen bereits weit verbreitet. Fur eine eingeschrankte Klasse von Systemen sind die auftretenden Verifikationsprobleme von Natur aus endlich and konnen effizient gelost werden. Fur komplexe Systeme kann eine solche Endlichkeit nicht angenommen werden. Um Eigenschaften solcher Systeme ausdrucken und beweisen zu konnen, brauchen wir eine formale Sprache und Beweismethoden, die mit universeller Quantifizierung, arithmetischen Ausdrucken und unbeschrankten Datentypen gleichzeitig umgehen konnen. Deshalb gab es in den letzten Jahren ein neues Interesse an Methoden, die universell quantifizierte Probleme in solchen Hintergrundtheorien losen konnen. Es ist bekannt, dass solche Probleme im Allgemeinen unentscheidbar sind, und die Forschung konzentriert sich auf Methoden, die unter Verzicht auf Vollstandigkeit moglichst viele Probleme schnell losen konnen. Wir verfolgen einen anderen Ansatz und konzentrieren uns auf Problemklassen, deren Entscheidbarkeit wir zeigen konnen. Dadurch konnen wir diese Probleme effizient losen 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 Pradikatenlogik erster Ordnung. Wir fuhren die Arbeit an lokalen Theorieerweiterungen fort, indem wir neue Beispiele von Axiomen geben, die eine Lokalitatseigenschaft erfullen, und benutzen Ideen aus instanziierungs-basierten Methoden zum Theorembeweisen in Pradikatenlogik, um lokales Beweisen effizienter zu machen. Weiterhin zeigen wir, dass lokale Theorieerweiterungen es uns ermoglichen, bestimmte Verifikationsprobleme fur 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.