Towards a comprehensive extension of abstract state machines for aspect-oriented specification

With the paradigm of aspect-orientation, a developer is able to separate the code of so-called cross-cutting concerns from the rest of the program's logic. This possibility is useful for formal specifications, too. For example, security aspects can be separated from the rest of the specification. Those aspect-oriented specifications often can be more easily reused than extensions that are implemented directly into an existing specification. Another use case is the extension of a specification with new functionality or features. Although this would be possible with refinement too, with aspect-orientation it is not necessary to augment the original specification with "extension points" that can be used for refinement. This paper describes the implementation of the aspect-oriented approach in Abstract State Machines. We introduce an aspect language with its syntax and formal semantics. It allows for specifying pointcuts where an original specification is augmented according to an aspect specification. Besides the general overview of this language extension, some ASM specific features of the realization are depicted in detail. The applicability of aspect oriented specification in the context of ASM is demonstrated by means of examples, e.g. implementing a fading aspect into the light control system specification of a former ASM case study. Finally, the paper gives a brief overview about the developed tool that supports the writing of aspect-oriented ASMs. (C) 2016 Elsevier B.V. All rights reserved.