Abstract

This work is an application, a projection of one research area into another. The first one is software validation. The need for proving certain properties about a program such as deadlock freedom or availability constraints evolved a long time ago when first program complexes of considerable size appeared. The first steps in proving correctness of computer programs were taken in the 1970s (e.g. communicating sequential processes and proof systems for them). Recently the new trend in this area was model-based methods where a computer was doing a man’s job. They were used for years in hardware verification, but only recently the computational power has made them applicable for software.

The second area of research of this work is distributed application development. With the growth of the Internet, single user and single machine applications are dying. Modern tendencies are about considering large heterogeneous portfolios of components that collaborate in providing a service to end users. One of the chapters of this work is dedicated to researching the influence this domain has on software verification and which parts of distributed applications can be efficiently verified.

To complete the picture, the last chapter is dedicated to the practical side of the issues. It presents practical analysis, comprehensive examination, model checking, verification, model refinement and repeated verification for three case studies. We will consider an untraceability protocol, an access management system and a transaction processing system. Each case study comprises a classic scheme and our own complicating extensions. This forms a practical basis of this work and demonstrates how the chosen methodology of model checking should be applied to distributed applications.