Dokument: Ein Modelchecker für CSP-M
| Titel: | Ein Modelchecker für CSP-M | |||||||
| Weiterer Titel: | A Model Checker for CSP-M | |||||||
| URL für Lesezeichen: | https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=20301 | |||||||
| URN (NBN): | urn:nbn:de:hbz:061-20120117-151955-7 | |||||||
| Kollektion: | Dissertationen | |||||||
| Sprache: | Englisch | |||||||
| Dokumententyp: | Wissenschaftliche Abschlussarbeiten » Dissertation | |||||||
| Medientyp: | Text | |||||||
| Autor: | Fontaine, Marc [Autor] | |||||||
| Dateien: |
| |||||||
| Beitragende: | Prof. Dr. Michael Leuschel [Gutachter] Prof. Dr. Heike Wehrheim [Gutachter] | |||||||
| Stichwörter: | CSP,CSP-M,FDR,Haskell,ProB,parallel computing | |||||||
| Dewey Dezimal-Klassifikation: | 000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik | |||||||
| Beschreibungen: | Diese Arbeit präsentiert ein neues Softwarewerkzeug zur Animation und zum Modelchecking von CSP-M. CSP-M ist eine Spezifikationssprache, aus dem Bereich der formalen Methoden, die von mehreren Werkzeugen unterstützt wird, z.B.
FDR und ProB. Sie basiert auf der Prozessalgebra kommunizierender sequenzieller Prozesse (engl. communicating sequential processes, CSP) von C.A.R. Hoare. Der Hauptbeitrag der Arbeit ist die detaillierte und umfassende Beschreibung eines neuen Werkzeugs für CSP-M. Die wichtigsten Designziele meines Werkzeugs sind Korrektheit, Modularität und Wiederverwendbarkeit. Ich beschreibe die Umsetzung der Designziele im Quellcode und erkläre die grundsä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 Parallelrechnerversion 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-M Semantik und als Baustein für zukünftige CSP-M Werkzeuge dienen.This thesis presents a new tool for the animation and model checking of CSP-M. CSP-M is the machine readable syntax for Hoare’s Communicating Sequential 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 discussion of a new CSP-M tool. The most important design goals for my CSP-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 language for the implementation of a formal methods tool. I explain how Haskell 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-M semantics and as a building block for future CSP-M tools. | |||||||
| Lizenz: |  Urheberrechtsschutz | |||||||
| Fachbereich / Einrichtung: | Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen | |||||||
| Dokument erstellt am: | 17.01.2012 | |||||||
| Dateien geändert am: | 17.01.2012 | |||||||
| Promotionsantrag am: | 31.01.2011 | |||||||
| Datum der Promotion: | 06.10.2011 |
