Dokument: New Applications and Techniques for Constraint Programming in B
| Titel: | New Applications and Techniques for Constraint Programming in B | |||||||
| URL für Lesezeichen: | https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=64042 | |||||||
| URN (NBN): | urn:nbn:de:hbz:061-20231110-105649-0 | |||||||
| Kollektion: | Dissertationen | |||||||
| Sprache: | Englisch | |||||||
| Dokumententyp: | Wissenschaftliche Abschlussarbeiten » Dissertation | |||||||
| Medientyp: | Text | |||||||
| Autor: | Schmidt, Joshua [Autor] | |||||||
| Dateien: |
| |||||||
| Beitragende: | Prof. Dr. Leuschel, Michael [Betreuer/Doktorvater] Privatdozent PhD Igor Konnov [Gutachter] | |||||||
| Stichwörter: | Formal Methods, Constraint Programming, Constraint Solving, B-Method, ProB, SAT Solving, SMT Solving, Constraint Logic Programming, Alloy, Z3, Model Checking | |||||||
| Dewey Dezimal-Klassifikation: | 000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik | |||||||
| Beschreibungen: | The safety of software systems is gaining importance due to the almost indispensable integration of software in modern everyday life. Formal methods are a fundamental approach for the design and verification of software and hardware systems, one of which is the B-Method. This thesis is a selection of my co-authored manuscripts on the B-Method and the ProB tool.
In the first part, a translation of a popular formal specification language called Alloy to classical B is presented, which is automated by ProB. A difference between both languages is that Alloy's syntax is flexible and resembles object-oriented programming languages while B's syntax is strictly typed and rooted in set theory, mathematics, and logic. In contrast to Alloy, B also allows defining infinite and arbitrarily nested sets and relations. Further, B has operational semantics, which eases the definition of state-based systems. Empirical results have shown benefits for performance and soundness of B and ProB compared to Alloy when solving integer constraints, and benefits for performance of the Alloy Analyzer compared to ProB when solving relational constraints. This work contributed to an ongoing discussion in the Alloy community to integrate state-based concepts in the core language of Alloy and Satisfiability Modulo Theories (SMT) in the Alloy Analyzer. Besides that, this work improved the communication between the Alloy and B communities. The second part of this thesis deals with constraint solving, which is one of the most important features of any formal verification tool. ProB's constraint solver has proven to be powerful for many problems. Yet, its use of plain saturation-based techniques often prevents finding contradictions, especially when considering infinite domains. We present additional constraint solving backends for ProB using techniques of SMT, which enable to learn from conflicts and leverage the power of Boolean satisfiability solving. In particular, we present an extended translation from B to SMT-LIB and integration of Z3 in ProB as well as a custom implementation of SMT in ProB. Empirical results have shown benefits of clause learning and abstractions to Boolean satisfiability solving compared to ProB's native constraint solver, especially when it comes to finding contradictions. For instance, it can be possible to identify a contradiction in a formula's Boolean abstraction without interpreting any theory constraint for which the satisfiability might be undecidable. Z3's theory solvers have further shown benefits in solving constraints involving infinite domains and integer arithmetic. The overall results, however, have shown that no constraint solver is the best for solving all kinds of constraints. For the verification of formal systems, it is thus beneficial to have a large portfolio of different constraint solving backends, as is the case for the ProB tool.Die Sicherheit von Softwaresystemen gewinnt durch die fast unverzichtbare Integration von Software in den modernen Alltag immer mehr an Bedeutung. Formale Methoden wie die B-Methode sind ein grundlegender Ansatz für den Entwurf und die Verifikation von Software- und Hardwaresystemen. Diese Arbeit ist eine Auswahl von Manuskripten zu der B-Methode und dem ProB Werkzeug, an denen ich grundlegend mitgewirkt habe. Im ersten Teil dieser Arbeit wird eine Übersetzung einer populären formalen Spezifikationssprache namens Alloy in die klassische B Sprache vorgestellt, welche mittels ProB automatisiert wird. Ein Unterschied zwischen beiden Sprachen ist, dass die Syntax von Alloy flexibel ist und objektorientierten Programmiersprachen ähnelt, während die Syntax von B streng typisiert ist und auf der Mengenlehre, Mathematik und Logik basiert. Darüber hinaus verfügt B über eine operative Semantik, welche die Definition von zustandsbasierten Systemen erleichtert. Empirische Ergebnisse haben Vorteile für die Leistung und Korrektheit von B und ProB im Vergleich zu Alloy beim Lösen ganzzahliger Arithmetik gezeigt. Der Alloy Analyzer hat eine bessere Leistung im Vergleich zu ProB beim Lösen relationaler Einschränkungen gezeigt. Diese Arbeit hat zu einer bestehenden Diskussion in der Alloy Community bezüglich der Integration von zustandsbasiertem Verhalten in der Kernsprache von Alloy sowie der Verwendung von Satisfiability Modulo Theories (SMT) beigetragen. Außerdem hat diese Arbeit die Kommunikation zwischen der Alloy- und der B-Community verbessert. Der zweite Teil dieser Arbeit befasst sich mit dem Constraint Solving, was eine der wichtigsten Fähigkeiten eines formalen Verifikationswerkzeug ist. Der Constraint Solver von ProB hat sich als leistungsfähig erwiesen. Die schiere Enumeration von Domänen verhindert jedoch häufig das Auffinden von Widersprüchen, insbesondere für unendliche Domänen. Wir präsentieren zusätzliche Constraint Solving Backends für ProB basierend auf SMT. Diese Techniken ermöglichen es, aus Konflikten zu lernen und die Vorteile des Lösens aussagenlogischer Formeln zu nutzen. Im Einzelnen präsentieren wir eine erweiterte Übersetzung von B nach SMT-LIB und Integration von Z3 in ProB sowie eine manuelle Implementierung von SMT. Empirische Ergebnisse haben Vorteile des Lernens von Klauseln und der Verwendung aussagenlogischer Abstraktionen im Vergleich zu ProB's Constraint Solver gezeigt, insbesondere für die Erkennung von Widersprüchen. Beispielsweise ist es möglich, dass ein Widerspruch in der booleschen Abstraktion einer Formel erkannt wird, ohne eine möglicherweise unentscheidbare Theoriebeschränkung zu interpretieren. Z3 hat außerdem Vorteile für das Lösen von Formeln mit unendlichen Domänen und ganzzahliger Arithmetik gezeigt. Insgesamt wurde jedoch deutlich, dass kein Constraint Solver der Beste ist, um alle Formeln zu lösen. Für die Verifikation formaler Systeme ist es daher von Vorteil über ein Portfolio unterschiedlicher Constraint Solver zu verfügen, wie dies bei dem ProB Werkzeug der Fall ist. | |||||||
| Lizenz: |  Dieses Werk ist lizenziert unter einer Creative Commons Namensnennung 4.0 International Lizenz | |||||||
| Fachbereich / Einrichtung: | Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen | |||||||
| Dokument erstellt am: | 10.11.2023 | |||||||
| Dateien geändert am: | 10.11.2023 | |||||||
| Promotionsantrag am: | 21.03.2023 | |||||||
| Datum der Promotion: | 24.07.2023 |
