A System for Compositional Verification of Asynchronous Objects

Wolfgang Ahrendt, Maximilian Dylla

We present 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. Building on KeY
characteristic concepts, like dynamic logic, sequent calculus,
symbolic execution via explicit substitutions, and the taclet rule
language, the presented system addresses functional correctness of
Creol models featuring local cooperative thread parallelism and global
communication via asynchronous method calls. The calculus heavily
operates on communication histories specified by the interfaces of
Creol units. Two example scenarios demonstrate the usage of the
system. This article extends the conference paper of Ahrendt and Dylla
(2009) with a denotational semantics of Creol and an
assumption-commitment style semantics of the logic.