Ein Modelchecker für CSP-M [Elektronische Ressource] / Marc Fontaine

Sujets

• Informatik

Informations

• Publié par: heinrich-heine-universitat_dusseldorf
• Publié le: 01 janvier 2012
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

A Model Checker for CSPM
Inaugural-Dissertation
zur Erlangung des Doktorgrades
der Mathematisch-Naturwissenschaftlichen Fakultät
der Heinrich-Heine-Universität Düsseldorf
vorgelegt von
Marc Fontaine
Düsseldorf, Juli 2011aus dem Institut für Informatik der Heinrich-Heine Universität Düsseldorf
gedruckt mit der Genehmigung der
Mathematisch-Naturwissenschaftlichen Fakultät der
Heinrich-Heine-Universität Düsseldorf
Referent: Prof. Dr. Michael Leuschel
Koreferent: Prof. Dr. Heike Wehrheim
Tag der mündlichen Prüfung: 6. Oktober 2011Abstract
This thesis presents a new tool for the animation and model checking of
CSP . CSP is the machine readable syntax for Hoare’s Communicating Se-M M
quential Processes. It is a specification language used by several formal methods
tools, for example FDR and ProB.
The main contribution of the thesis is the detailed and comprehensive dis-
cussion of a new CSP tool. The most important design goals for my CSPM M
tool are correctness, modularity and reusability. I describe how the design goals
are reflected in the source code and explain the basic design decisions that were
taken. I also compare the features and performance of the new tool with ProB
and FDR and I present some benchmarks for a multi-core version of my tool.
This thesis is also a case study for the use of the Haskell programming
languagefortheimplementationofaformalmethodstool. IexplainhowHaskell
has influenced the design and how Haskell helps to achieve the design goals of
my software. The presented software can serve as a reference implementation
of the CSP semantics and as a building block for future CSP tools.M M
Kurzreferat
Diese Arbeit präsentiert ein neues Softwarewerkzeug zur Animation und zum
Modelchecking von CSP . CSP ist eine Spezifikationssprache, aus dem Bere-M M
ichderformalenMethoden, dievonmehrerenWerkzeugenunterstütztwird, z.B.
FDR und ProB. Sie basiert auf der Prozessalgebra kommunizierender sequen-
zieller Prozesse (engl. communicating sequential processes, CSP) von C.A.R.
Hoare.
Der Hauptbeitrag der Arbeit ist die detaillierte und umfassende Beschrei-
bung eines neuen Werkzeugs für CSP . Die wichtigsten Designziele meinesM
Werkzeugs sind Korrektheit, Modularität und Wiederverwendbarkeit. Ich be-
schreibe die Umsetzung der Designziele im Quellcode und erkläre die grund-
sätzlichen Designentscheidungen, die getroffen wurden. Außerdem vergleiche
ich die Eigenschaften und die Leistungsfähigkeit meines neuen Werkzeugs mit
ProB und FDR und zeige mehrere Laufzeitmessungen für eine Parallelrechn-
erversion meines Programms.
Diese Arbeit ist auch eine Fallstudie über die Verwendung von Haskell als
Programmiersprache für Werkzeuge im Bereich der formalen Methoden. Ich
beschreibe wie Haskell das Design meiner Software beeinflusst hat und wie
Haskell dazu beiträgt, die Designziele zu erreichen. Die erstellte Software kann
als eine Referenzimplementierung für die CSP Semantik und als Baustein fürM
zukünftige CSP Werkzeuge dienen.MVorwort
Die vorliegende Dissertationsschrift entstand zwischen Februar 2010 und Juli
2011. Meine Zeit als wissenschaftlicher Mitarbeiter am Lehrstuhl für Soft-
waretechnik und Programmiersprachen begann Mitte 2005 und circa Mitte 2006
kam ich zum ersten Mal mit CSP, dem späteren Thema meiner Doktorarbeit, in
Kontakt. Ich danke allen, die in dieser Zeit dazu beigetragen haben, dass diese
Doktorarbeit erfolgreich beendet wurde.
Insbesondere danke ich Herrn Prof. Dr. Michael Leuschel für seine fre-
undliche, großzügige und geduldige Unterstützung. Ohne die finanzielle Ab-
sicherungalswissenschaftlicherMitarbeiterwäredieseDoktorarbeitnichtmöglich
gewesen.
SpezielldankeichHerrnJanusTomaschewskifürseinegroßeHilfbereitschaft,
die ich bei verschiedenen Gelegenheiten in Anspruch genommen habe. Herrn
Ivaylo Dobrikov danke ich für die Zusammenarbeit in Rahmen seiner Masterar-
beit.
Des Weitern danke ich Jens Bendisposto, Daniel Plagge, Michael Jastram,
Carl Friedrich Bolz und allen Mitarbeitern und Mitarbeiterinnen des Lehrstuhls
für Softwaretechnik und Programmiersprachen und des Fachbereiches Infor-
matik Heinrich-Heine-Universität für die freundliche Zusammenarbeit.
Eine große Motivation für mich war die Kooperation über den Lehrstuhl
hinaus. Ich bedanke mich bei allen, die meine Software ausprobiert, getestet
und Rückmeldungen dazu gegeben haben. In dem Zusammenhang möchte ich
Moritz Kleine, Diego Oliveira, Marc Dragon, Philip Armstrong, Edward Turner
und Robert Colvin nennen.Contents
1 Introduction 9
1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2 CSP 12
2.1 Informal Introduction to CSP . . . . . . . . . . . . . . . . . . . . 12
2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.1 Algebraic Semantics . . . . . . . . . . . . . . . . . . . . . 15
2.2.2 Denotational Semantics . . . . . . . . . . . . . . . . . . . 15
2.2.3 Operationaltics and Firing Rules . . . . . . . . . . 16
2.3 Extensions of Core CSP . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.1 Multi-field Events and Data . . . . . . . . . . . . . . . . . 19
2.3.2 Event Patterns . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3.3 Data Processing . . . . . . . . . . . . . . . . . . . . . . . 20
2.3.4 Mixing Input and Output Fields . . . . . . . . . . . . . . 20
2.3.5 Parametrised Processes . . . . . . . . . . . . . . . . . . . 20
2.3.6 Complete Functional Process Definition . . . . . . . . . . 21
2.4 Formal Definition of CSP . . . . . . . . . . . . . . . . . . . . . 21M
3 Software Architecture of the CSP Tool 22M
3.1 The Haskell Programming Language . . . . . . . . . . . . . . . . 22
3.2 Architecture Overview . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3 Source Code Included in the Thesis . . . . . . . . . . . . . . . . . 25
3.3.1 Hints for Understanding the Code . . . . . . . . . . . . . 26
3.3.2 Type Families . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.4 Role of Haskell . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.5 Haskell Critique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4 Modeling of the CSP Core Language in Haskell 32
4.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4.1.1 Modeling of Processes . . . . . . . . . . . . . . . . . . . . 32
4.1.2 Mo of Events . . . . . . . . . . . . . . . . . . . . . . 34
4.1.3 Example of the Modeling of Processes . . . . . . . . . . . 35
4.2 Implementation of the Operational Semantics . . . . . . . . . . . 36
4.2.1 Section Outline . . . . . . . . . . . . . . . . . . . . . . . . 36
4.2.2 Advantages of Explicit Proof Trees . . . . . . . . . . . . . 37
4.2.3 Modeling of Proof Trees . . . . . . . . . . . . . . . . . . . 38
4.2.4 Generation of Proof Trees for τ andX . . . . . . . . . . . 42
54.2.5 Naïve Generation of Proof Trees for Regular Transitions . 46
4.3 Constraint-Based of Proof Trees . . . . . . . . . . . . 49
4.3.1 Generating the Initial Proof Tree Skeletons . . . . . . . . 52
4.3.2 Constraint Propagation . . . . . . . . . . . . . . . . . . . 54
4.3.3 Fixing a Field Value in the Proof Tree Skeleton . . . . . . 55
4.3.4 Converting a Proof Tree Skeleton to a Proof Tree . . . . . 56
4.3.5 The Main Loop . . . . . . . . . . . . . . . . . . . . . . . . 56
4.3.6 Modeling Multi-field Events . . . . . . . . . . . . . . . . . 58
4.3.7 Event Sets for Multi-field Events . . . . . . . . . . . . . . 59
4.3.8 Critique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.4 Testing the Implemented Semantics with QuickCheck . . . . . . 61
4.4.1 Proof Tree Verifier as a Specification of the Proof Tree
Generator . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.4.2 EqualityoftheNaïveProofTreeGeneratorandtheConstraint-
based Proof Tree Generator . . . . . . . . . . . . . . . . . 64
4.4.3 Code Coverage Analysis . . . . . . . . . . . . . . . . . . . 65
4.4.4 Mock Implementations . . . . . . . . . . . . . . . . . . . . 65
4.4.5 QuickCheck Conclusion . . . . . . . . . . . . . . . . . . . 65
4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
5 Interpreter for the Functional Sub-language of CSP 67M
5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
5.1.1 External Interface of the Interpreter . . . . . . . . . . . . 68
5.2 Design Decisions for the Interpreter . . . . . . . . . . . . . . . . . 68
5.2.1 FDR Compatibility . . . . . . . . . . . . . . . . . . . . . 68
5.2.2 Model Checking and Equality . . . . . . . . . . . . . . . . 69
5.2.3 Interpreter and Denotational Semantics . . . . . . . . . . 70
5.2.4 Environment vs. HOAS . . . . . . . . . . . . . . . . . . . 70
5.2.5 CSP Laziness . . . . . . . . . . . . . . . . . . . . . . . . 71M
5.2.6 Using Haskell Laziness and Knot-Tying . . . . . . . . . . 72
5.2.7 Lambda-lifting . . . . . . . . . . . . . . . . . . . . . . . . 72
5.2.8 Pure Interpreter . . . . . . . . . . . . . . . . . . . . . . . 73
5.2.9 Representing CSP Values . . . . . . . . . . . . . . . . . 73M