Contract-Based Specification and Analysis of AADL Models.
Ernesto Posse, Jürgen Dingel · 2014
Abstract. We describe an approach to the specification, analysis and verification of AADL models using assume/guarantee behavioural con-tracts specified with the Property Specification Language (PSL). This approach aids the development process by 1) supporting the reuse and replacement of components based on their contracts rather than only their interface or their implementation and thus reducing the need for re-engineering; 2) providing early discovery of behavioural inconsistencies that may pose problems with integration; and 3) allowing an incremen-tal and flexible application of specification and verification instead of requiring an all-or-nothing approach. It also helps improving the prod-uct itself by detecting safety and liveness problems via model-checking. We also briefly discuss a prototype plug-in for OSATE supporting an annex language which we call AGCL. 1