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

A Model Checker for CSPMInaugural-Dissertationzur Erlangung des Doktorgradesder Mathematisch-Naturwissenschaftlichen Fakultätder Heinrich-Heine-Universität Düsseldorfvorgelegt vonMarc FontaineDüsseldorf, Juli 2011aus dem Institut für Informatik der Heinrich-Heine Universität Düsseldorfgedruckt mit der Genehmigung derMathematisch-Naturwissenschaftlichen Fakultät derHeinrich-Heine-Universität DüsseldorfReferent: Prof. Dr. Michael LeuschelKoreferent: Prof. Dr. Heike WehrheimTag der mündlichen Prüfung: 6. Oktober 2011AbstractThis thesis presents a new tool for the animation and model checking ofCSP . CSP is the machine readable syntax for Hoare’s Communicating Se-M Mquential Processes. It is a specification language used by several formal methodstools, 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 Mtool are correctness, modularity and reusability. I describe how the design goalsare reflected in the source code and explain the basic design decisions that weretaken. I also compare the features and performance of the new tool with ProBand 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 programminglanguagefortheimplementationofaformalmethodstool.