Verification of distributed applications

Abstract

Safety and security guarantees for individual applications in almost all cases depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs running on these. In particular for formal approaches the problem is to formalize these assumptions without looking at the (formal) model of the operating system (including the machines that execute applications) in all detail. The work described in the paper proposes a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. As an example the paper discusses the specification and implementation of the SMTP scenario. It shows in detail how this methodology is utilized within the Verification Support Environment (VSE) to verify the SMTP server part. © Springer-Verlag Berlin Heidelberg 2007.