Specification patterns: formal and easy

FERNANDO ASTEASUAIN; VICTOR A. BRABERMAN

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING

WORLD SCIENTIFIC PUBL CO PTE LTD

Lugar: London, UK; Año: 2015 vol. 25 p. 669 - 700

0218-1940

Property specication is still one of the most challenging tasks for transference of soft- ware verication technology. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satised. When validating the desired property the developer may have to deal with the pattern representation in some particular formalism. For this reason, we identify four desirable quality attributes for the underlying specication language: succinctness, comparability, complementariness, and modiability. We show that typ- ical formalisms such as temporal logics or automata fail at some extent to support these features. Given this context we introduce Featherweight Visual Scenarios (FVS), a declarative and graphical language based on scenarios, as a possible alternative to specify behavioral properties. We illustrate FVS applicability by modeling all the speci- cation patterns and we thoroughly compare FVS to other known approaches, showing that FVS specications are better suited for validation tasks. In addition, we augment pattern specication by introducing the concept of violating behavior. Finally we char- acterize the type of properties that can be written in FVS and we formally introduce its syntax and semantics.