PROBE: Proof Obligations for Aspect-Oriented Systems

Principal Investigator: Awais Rashid
Project Personnel: Prof. Shmuel Katz (Visiting Fellow)
Project Description
Related Publications
Grant Ref: EPSRC GR/S70159/01
Start Date: September 2003
End Date: February 2004

Project Description:
The project aims to establish concrete connections between aspectual requirements, UML design specifications of aspects and the code implementing these specifications. More specifically, the project aims to:

• develop a proof obligation framework for precise analysis of aspect-oriented systems using formal verification tools;
• design a tool supporting the proof obligation framework.

The framework will provide means to define proof obligations (about the implementation) that follow from aspectual requirements and their corresponding UML design description. The tool will provide the interface between requirements and design level aspects, and generate properties to be checked in the form of input expected by an existing software verification tool.

Publications:

• Katz, S. and A. Rashid (2004) From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. International Conference on Requirements Engineering (RE), Kayoto, Japan. IEEE Computer Society Press. Pages 48-57. Pdf link.
• Katz, S. and A. Rashid (2004) PROBE: From Requirements and Design to Proof Obligations for Aspect-Oriented Systems. Computing Department Lancaster University Technical Report Number: COMP-002-2004. Pdf link.