transparent gif


Ej inloggad.

Göteborgs universitets publikationer

Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar

Författare och institution:
M. Autili (-); L. Grunske (-); M. Lumpe (-); Patrizio Pelliccione (Institutionen för data- och informationsteknik (GU)); A. Tang (-)
Publicerad i:
IEEE Transactions on Software Engineering, 41 ( 7 ) s. 620-638
Artikel, refereegranskad vetenskaplig
Sammanfattning (abstract):
Formal methods offer an effective means to assert the correctness of software systems through mathematical reasoning. However, the need to formulate system properties in a purely mathematical fashion can create pragmatic barriers to the application of these techniques. For this reason, Dwyer et al. invented property specification patterns which is a system of recurring solutions to deal with the temporal intricacies that would make the construction of reactive systems very hard otherwise. Today, property specification patterns provide general rules that help practitioners to qualify order and occurrence, to quantify time bounds, and to express probabilities of events. Nevertheless, a comprehensive framework combining qualitative, real-time, and probabilistic property specification patterns has remained elusive. The benefits of such a framework are twofold. First, it would remove the distinction between qualitative and quantitative aspects of events; and second, it would provide a structure to systematically discover new property specification patterns. In this paper, we report on such a framework and present a unified catalogue that combines all known plus 40 newly identified or extended patterns. We also offer a natural language front-end to map patterns to a temporal logic of choice. To demonstrate the virtue of this new framework, we applied it to a variety of industrial requirements, and use PSPWizard, a tool specifically developed to work with our unified pattern catalogue, to automatically render concrete instances of property specification patterns to formulae of an underlying temporal logic of choice.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
Data- och informationsvetenskap ->
Elektroteknik och elektronik
Specification patterns, real-time properties, probabilistic properties
Postens nummer:
Posten skapad:
2015-08-14 15:11
Posten ändrad:
2016-09-13 10:54

Visa i Endnote-format

Göteborgs universitet • Tel. 031-786 0000
© Göteborgs universitet 2007