Specification patterns for probabilistic quality properties

Abstract

Probabilistic verification techniques are a powerful means to ensure that a software-intensive system fulfills its quality requirements. To apply these techniques an accurate specification of the required properties in a probabilistic temporal logic is necessary. To help practitioners formulate these properties correctly, this paper presents a specification pattern system of common probabilistic properties called ProProST. This pattern system has been a developed based on a survey of 152 properties from academic examples and 48 properties of real-word quality requirements from avionic, defence and automotive systems. Furthermore, a structured English grammar that can guide in the specification of probabilistic properties is given. Similar to previous specification patterns for traditional and real-time properties, the presented specification pattern system and the structured English grammar captures expert knowledge and helps practitioners to correctly apply formal verification techniques.

BibTeX

@inproceedings{Grunske:ICSE08,
  author    = {Lars Grunske},
  title     = {Specification patterns for probabilistic quality properties},
  booktitle = {ICSE},
  pages     = {31--40},
  publisher = {{ACM}},
  year      = {2008},
}

Specification patterns for probabilistic quality properties

Abstract

Related papers