Efficient computer-aided verification of parallel and distributed software systems
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
Doctoral thesis (article-based)
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
2003-11-28
Major/Subject
Mcode
Degree programme
Language
en
Pages
63, [81]
Series
Research reports / Helsinki University of Technology, Laboratory for Theoretical Computer Science. A, 81
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.Description
Keywords
distributed systems, software systems, model checking, verification, reachability analysis
Other note
Parts
- 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. [article1.pdf] © 2001 Springer-Verlag. By permission.
- 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. [article2.pdf] © 2002 Springer-Verlag. By permission.
- 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. [article3.pdf] © 2002 Australian Computer Society, Inc. By permission.
- 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. [article4.pdf] © 2003 Springer-Verlag. By permission.
- 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. [article5.pdf] © 2002 by authors.