Compositional Verification of Distributed Objects with Asynchronous Method Calls

Abstract: This talk presents a semantics, calculus, and system for compositional verification of Creol, an object-oriented modelling language for concurrent distributed applications. The system is an instance of KeY, a framework for object-oriented software verification, which has so far been applied foremost to sequential Java. The work presented in this talk addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus operates on communication histories specified by the interfaces of Creol units. A trace semantics of Creol and an assumption-commitment style semantics of the logic are introduced briefly.