Department of Information Technology

Compositional Verification of Distributed Objects with Asynchronous Method Calls

Speaker

Wolfgang Ahrendt, Chalmers / Göteborg University

Date and Time

Tuesday, May 31st, 2011 at 10:30

Location

Polacksbacken, room 1145

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.

Back to the seminar page

Updated  2011-05-12 13:50:13 by Frédéric Haziza.