The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
Aalto

Efficient Computer-Aided Verification of Parallel and Distributed Software Systems

Marko Mäkelä

Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Department of Computer Science and Engineering for public examination and debate in Auditorium E at Helsinki University of Technology (Espoo, Finland) on the 28th of November, 2003, at 12 o'clock noon.

Overview in PDF format (ISBN 951-22-6792-6)   [760 KB]
Dissertation is also available in print (ISBN 951-22-6791-8)

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.

This thesis consists of an overview and of the following 5 publications:

  1. Mäkelä M., 2001. Optimising enabling tests and unfoldings of algebraic system nets. In: Colom J.-M. and Koutny M. (Eds.), Application and Theory of Petri Nets 2001, 22nd International Conference (ICATPN 2001). Newcastle upon Tyne, England, June 2001. Springer-Verlag, Berlin. Lecture Notes in Computer Science 2075, pages 283-302. © 2001 Springer-Verlag. By permission.
  2. Mäkelä M., 2002. MARIA: Modular reachability analyser for algebraic system nets. In: Esparza J. and Lakos C. (Eds.), Application and Theory of Petri Nets 2002, 23rd International Conference (ICATPN 2002). Adelaide, Australia, June 2002. Springer-Verlag, Berlin. Lecture Notes in Computer Science 2360, pages 434-444. © 2002 Springer-Verlag. By permission.
  3. Mäkelä M., 2002. Efficiently verifying safety properties with idle office computers. In: Lakos C., Esser R., Kristensen L. M. and Billington J. (Eds.), Formal Methods in Software Engineering and Defence Systems 2002. Adelaide, Australia, June 2002. Australian Computer Society, Inc. Conferences in Research and Practice in Information Technology 12, pages 11-16. © 2002 Australian Computer Society, Inc. By permission.
  4. Mäkelä M., 2003. Model checking safety properties in modular high-level nets. In: van der Aalst W. M. P. and Best E. (Eds.), Application and Theory of Petri Nets 2003, 24th International Conference (ICATPN 2003). Eindhoven, The Netherlands, June 2003. Springer-Verlag, Berlin. Lecture Notes in Computer Science 2679, pages 201-220. © 2003 Springer-Verlag. By permission.
  5. Järvenpää J. and Mäkelä M., 2002. Towards automated checking of component-oriented enterprise applications. In: Moldt D. (Ed.), Second Workshop on Modelling of Objects, Components and Agents. University of Århus, Denmark, August 2002. DAIMI report PB-561, pages 67-85. © 2002 by authors.

Errata of publications 1 and 3

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

This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.

© 2003 Helsinki University of Technology

Last update 2011-05-26