Verification of Assertions in Creol Programs

Abstract

Open distributed systems are composed of geographically dispersed components that may be modified at run-time. Such systems are becoming increasingly important, particularly when they are part of the infrastructure used by safety-critical applications. Creol is an experimental object-oriented programming language designed for modeling such systems. Creol objects execute concurrently, each with its own virtual processor and internal process control, and communication takes place using asynchronous (non-blocking) method calls.

To increase the reliability of the systems in which they operate, Creol classes make explicit assumptions about their environment and provide guarantees about their own behavior. The assume-guarantee paradigm enables scalable, compositional verification based on invariance. The goal of this thesis is to implement a tool that verifies assume-guarantee specifications and other program assertions using Maude, an established rewriting logic framework. The tool takes a set of Creol classes and interfaces as input, and uses Hoare logic to generate verification conditions that can be discharged using off-the-shelf theorem provers.