Probabilistic Property Specification Templates
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. ProProST has been developed to help practitioners formulate these properties correctly. 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.
Grunske L., Specification Patterns for Probabilistic Quality Properties. 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008. ACM 2008, ISBN 978-1-60558-079-1, pp. 31-40.