A History-based Verification of Distributed Applications

Safety and security guarantees for individual applications in general depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs that are executed on these platforms. The problem for formal approaches is to formalize these assumptions without having to look at the details of the (formal) model of the operating system (including the machines that execute applications). The work described in this paper presents 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. In this paper we focus on this methodology and on its realization in the Verification Support Environment (VSE). We also illustrate the proposed approach with the help of a suitable example, namely the specification and verification ...

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Bruno Langenstein, Andreas Nonnengart, Georg Rock, Werner Stephan
• Keywords: Application Level Programs, Automated Reasoning, CADE 2007, Distributed Instances, Verification Support Environment