CPL - Chalmers Publication Library

Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving

Författare och institution:
Hans Svensson (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Serie:
1) Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, ISSN 0346-718X; nr 2777
2) Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, ISSN 1653-1787; nr 38D
ISBN:
978-91-7385-096-4
Antal sidor:
212
Publikationstyp:
Doktorsavhandling
Förlag:
Chalmers University of Technology
Förlagsort:
Göteborg
Publiceringsår:
2008
Språk:
engelska
Datum för examination:
2008-04-21
Tidpunkt för examination:
10:15
Lokal:
HC1, Hörsalsvägen 14
Opponent:
Prof. Jaco van de Pol, Formal Methods and Tools, Universiteit Twente, The Netherlands
Inkluderade delarbeten:
Sammanfattning (abstract):
Software infiltrates every aspect of modern society. Production, transportation, entertainment, and almost every other sphere that influences modern living are either directly or indirectly dependent on software systems. Software systems provide such a degree of flexibility that their role as a driving force for new and better products is indisputable. The downside is that software systems are rarely error-free. For a plentitude of reasons most software systems contain errors. Software errors impose large costs; the more important the system, the higher is the cost of an error. Reports show that a normal software development project spends 40% to 50% of its time and budget on quality assurance. Thus, software project economy is a great incitament for research of better tools and methods for software development. This thesis is part of the continuous efforts of finding more efficient software development methods and addresses the problem of verifying algorithm implementations. We have in particular studied algorithms designed for distributed (systems composed of a collection of computers, processors or processes) and fault-tolerant systems (systems designed to withstand some degree of failure). Verification of distributed and fault-tolerant systems is notoriously hard because both the distribution and the fault-tolerance add complexity to the software systems. The thesis introduces, motivates and evaluates several different verification methods related to distributed and fault-tolerant algorithm implementations. We introduce a trace-based testing method, which has been used to find and analyze errors in an existing open-source implementation of a fault-tolerant leader election algorithm. In the thesis we also present a new open-source implementation of a leader election algorithm, which is based on a verified algorithm by Stoller. We have developed a distributed semantics for Erlang. Errors found using trace-based testing indicated that existing Erlang semantics were not detailed enough. We propose a fully distributed extension of an existing single-node semantics for Erlang. We present McErlang, an explicit state model checker implemented in Erlang, and using Erlang as its specification language. We demonstrate that the 'all in Erlang'-approach to model checking is promising. We propose a semi-automatic algorithm verification method that has been used to prove safety properties for Stoller's leader election algorithm. The verification method uses automated theorem provers to inductively prove first-order logic invariants.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Programvaruteknik
Nyckelord:
verification, testing, model checking, theorem proving, Erlang, distributed programming, distributed algorithms, fault-tolerance
Postens nummer:
69328
Posten skapad:
2008-03-18 13:21
Posten ändrad:
2013-09-25 15:19

Visa i Endnote-format