Efficient Computer-Aided Verification of Parallel and Distributed Software Systems

Reference:

Marko Mäkelä. Efficient computer-aided verification of parallel and distributed software systems. Research Report A81, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, November 2003. Doctoral dissertation.

Abstract:

The society is becoming increasingly dependent on applications of distributed software systems, such as controller systems and wireless telecommunications. It is very difficult to guarantee the correct operation of this kind of systems with traditional software quality assurance methods, such as code reviews and testing. Formal methods, which are based on mathematical theories, have been suggested as a solution. Unfortunately, the vast complexity of the systems and the lack of competent personnel have prevented the adoption of sophisticated methods, such as theorem proving.

Computerised tools for verifying finite state asynchronous systems exist, and they been successful on locating errors in relatively small software systems. However, a direct translation of software to low-level formal models may lead to unmanageably large models or complex behaviour. Abstract models and algorithms that operate on compact high-level designs are needed to analyse larger systems.

This work introduces modelling formalisms and verification methods of distributed systems, presents efficient algorithms for verifying high-level models of large software systems, including an automated method for abstracting unneeded details from systems consisting of loosely connected components, and shows how the methods can be applied in the software development industry.

Keywords:

distributed systems, software systems, model checking, verification, reachability analysis

Suggested BibTeX entry:

@techreport{HUT-TCS-A81,
    address = {Espoo, Finland},
    author = {Marko M\"akel\"a},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {November},
    note = {Doctoral dissertation},
    number = {A81},
    pages = {63+76},
    title = {Efficient Computer-Aided Verification of Parallel and Distributed Software Systems},
    type = {Research Report},
    year = {2003},
}