Loading...
Please wait, while we are loading the content...
An Automatable Framework for Formal Specification & Verification of Aspect Oriented Programs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Qamar, Muhammad Nafees Nadeem, Aamer Khan, Muhammad Uzair |
| Copyright Year | 2006 |
| Abstract | Formal verification of software is a perennial problem and an inclusion to formal verification challenges is AOP (Aspect Oriented programs). Likewise, several contrary formal verification approaches exist for OOP (Object Oriented programs) but unable to deliver same robus tness for AOP verification and also the proposed approaches to verify AOP seem to be less effective because of their adoptability for large syste ms. Although we believe that the potential solution would be to choose best existing f ormal methods for formal verification of AOP to avoid unnecessary additions and m o ifications in current state of the art. This paper gives a thorough surv ey of the existing work. The paper presents a holistic framework for formal veri ficat on of AOP by formally specifying aspects and classes, autonomously. Then the obtained specifications are integrated to get filtered definition of the AOP, i.e., merging the aspect specification with the class specification to pre serv execution order of an AO program. Besides, to verify augmented system, the derivation of classes through de-compilation from compiled AOP is attaine d for generating their corresponding formal specifications. Former and latte r generated formal specifications are compared to analyze the intended and exotic behavior of aspects. This helps us to ensure that the actual behavior of the system is according to the one specified. Additionally, our approach helps to identify ambiguities and contradictions present in the compiled AOP, and a llows to eliminate them. We use Object-Z to write classes and pr opose our own notations and constructs for describing aspects and for form ulating filtered formal specification of classes and aspects using the notio n f filters from RTOZ (Real Time Object-Z ∗). A possible tool support realizes the automation process of the framework. *is a senior member of Center for Software Dependabil ity and presently working as Research Associate at COMSATS Institute of Informati on Technology, Islamabad. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.colostate.edu/csduml2006/CSDUML06FinalPapers/nr4_side39-52.pdf |
| Alternate Webpage(s) | http://www.researchgate.net/profile/Aamer_Nadeem/publication/228793664_An_Automatable_Framework_for_Formal_Specification__Verification_of_Aspect_Oriented_Programs/links/02e7e5152aae68eaf7000000.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
