The impact of aspect-oriented programming on formal methods

Abstract

This work considers the principles of aspect-oriented programming and applies them to formal methods. There are many different formal languages and it is clear that they exhibit great diversity both with respect to the style of language (syntax and semantics) and the domain of applicability. However, in general, it is unrealistic to expect to use a single language to specify the whole of a large and complex system. One problem is that, for systems exhibiting realtime, hybrid and/or stochastic behaviour, the functional (qualitative) behaviour of the system and the quantitative behaviour become entwined, or tangled together, in the specification. In our approach, each aspect may be specified using a different formal language. We can then (automatically) compose the different aspects together, serving a similar role to that of aspect-weaving. The resulting specification can be viewed textually or graphically, simulated or verified correct with respect to temporal logic formulae. For further information on our work, see http://www.comp.lancs.ac.uk/computing/users/lb/v-qos.html.