AVABI: Automated validation for behavioral interfaces of asynchronous active objects (completed)
The Avabi-project is funded as a bilateral Norwegian-German cooperation within the PPP-programme for collaborative research support scheme (``Projektbezogener Personenaustausch''). The cooperation is funded by the
The planned duration of the project is 24 months, the funding period spans the years 2008 and 2009.
For further information see the the project homepage.
In a nutshell
A strong current trend in software is towards component-based object-oriented systems, as they promise compositional development and deployment of software. Integral part of any component-based and compositional system description is the notion of interface, and recently, so-called behavioral interface descriptions, have begun to find acceptance, where ``behavioral'' refers to properties going beyond simple static properties like availability of methods or matching parameters. In this project we develop an appropriate behavioral interface description language for Creol, an object-oriented, concurrent programming language based on active objects, which is being developed at the University of Oslo. The formal interface description is intended as the core of a component-model for Creol, and using the interface language, we will develop and apply automated validation techniques. Beyond developing appropriate interface abstractions, the project will enhance the Creol-language by facilities for testing and simulation, extending the current Creol-implementation in the rewrite-engine Maude, resp. extending previous work for Java to the Creol setting. In addition, we apply model-checking to check interface conformance, following the well-established methodology of counter-example guided abstraction refinement.