CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Verification System for Distributed Objects with Asynchronous Method Calls

Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Maximilian Dylla
Formal Methods and Software Engineering, International Conference on Formal Engineering Methods, ICFEM'09 (0302-9743). Vol. 5885 (2009), p. 387-406.
[Konferensbidrag, refereegranskat]

We present a verification system for Creol, an object-oriented modeling 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, explicit substitutions, and the taclet rule language, the system presented in this paper 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 which describe the interfaces of Creol units. Two example scenarios demonstrate the usage of the system.



Denna post skapades 2009-12-18. Senast ändrad 2016-07-06.
CPL Pubid: 104371

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Datalogi

Chalmers infrastruktur