Specification Patterns: Formal and Easy
Abstract
Property specification is still one of the most challenging tasks for transference of software verification 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 satisfied. 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 specification language: succinctness, comparability, complementariness, and modifiability. We show that typical 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 specification patterns and we thoroughly compare FVS to other known approaches, showing that FVS specifications are better suited for validation tasks. In addition, we augment pattern specification by introducing the concept of violating behavior. Finally we characterize the type of properties that can be written in FVS and we formally introduce its syntax and semantics.
This work was partially funded by ANPCYT PICT 1774/11 and 0724/12, UBACYT W0813, UBACYT 20020130100384BA and MEALS 295261. Víctor Braberman is also affiliated to CONICET.
References
A. Alfonso , Visual timed event scenarios, 6th ICSE'04 (2004) pp. 168–177. Google Scholar- Software Engineering and Knowledge Engineering (SEKE) 430 ( 2010 ) . Google Scholar
- ASE 14(3), 293 (2007). Web of Science, Google Scholar
- ENTCS 211 , 147 ( 2008 ) . Google Scholar
-
V. Braberman , Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis , FORMATS ( Springer , 2009 ) . Google Scholar - IEEE TSE 31(12), 1028 (2005). Google Scholar
-
E. Clarke , O. Grumberg and D. Peled , Model Checking ( MIT Press , 1999 ) . Google Scholar R. Cobleigh , G. Avrunin and L. Clarke , User guidance for creating precise and accessible property specifications, Proc. of 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (2006) p. 218. Google ScholarS. Dalal , Model-based testing in practice, ICSE (1999) pp. 285–294. Google Scholar- ACM Trans. Software Engineering and Methodology 3(2), 131 (1994). Crossref, Google Scholar
-
N. D'Ippolito , Synthesis of Live Behaviour Models , Proc. of 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering ( 2010 ) . Google Scholar - M. Dwyer, G. Avrunin and J. Corbett, Specification Patterns Web Site, in http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml . Google Scholar
-
M. Dwyer , G. Avrunin and J. Corbett , Patterns in property specifications for finite-state verification , Proc. of 21st International Conference on Software Engineering (ICSE) 99 ( 1999 ) . Google Scholar D. Giannakopoulou and J. Magee , Fluent model checking for event-based systems, Proc. of 9th European Software Engineering Conference (2003) p. 266. Google ScholarM. Grohe and N. Schweikardt , The succinctness of first-order logic on linear orders, in Logic in Computer Science, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (2004) pp. 438–447. Google ScholarD. Harel and R. Marelly , Playing with time: On the specification and execution of time-enriched lscs, MASCOTS '02 (2002) pp. 193–202. Google Scholar- ACM Software Engineering Notes 27(6), 81 (2002). Crossref, Google Scholar
S. Konrad and B. Cheng , Real-time specification patterns, Proc. of 27th ICSE (2005) pp. 372–381. Google ScholarF. Laroussinie , N. Markey and P. Schnoebelen , Temporal logic with forgettable past, Proceedings-Symposium on Logic in Computer Science (2002) pp. 383–392. Google Scholar- ACM SIGSOFT Software Engineering Notes 31(3), 1 (2006). Crossref, Google Scholar
Z. Manna and A. Pnueli , A Hierarchy of Temporal Properties, Proc. of Ninth ACM PODC (1987) pp. 205–205. Google ScholarZ. Manna and A. Pnueli , Completing the temporal picture, Automata, Languages and Programming (1989) pp. 534–558. Google Scholar-
Z. Manna and A. Pnueli , A Temporal Proof Methodology for Reactive Systems ( Springler-Verlag , 1995 ) . Crossref, Google Scholar - EATCS Bull 79 , 122 ( 2003 ) . Google Scholar
- Commun. ACM 15(12), 1053 (1972). Crossref, Web of Science, Google Scholar
-
D. Paun and M. Chechik , Events in linear-time properties , Proc. of 4th International Conference on Requirements Engineering ( 1999 ) . Google Scholar - N. Piterman, A. Pnueli and Y. Sa'ar, Synthesis of reactive (1) designs, in Lecture Notes in Computer Science, Vol. 3855, 2006, pp. 364–380 . Google Scholar
-
M. Pradella , Practical model checking of LTL with past , ATVA03 ( 2003 ) . Google Scholar - , Implementing protocols via declarative event patterns, ACM Sigsoft International Symposium on FSE (2004) pp. 158–169. Google Scholar
B. Sengupta and R. Cleaveland , Triggered message sequence charts, SIGSOFT FSE (2002) pp. 167–176. Google ScholarM. Smith , G. Holzmann and K. Etessami , Events and constraints: A graphical editor for capturing logic requirements of programs, Proc. of 5th IEEE RE (2001) pp. 14–22. Google ScholarR. Smith , Propel: An approach supporting property elucidation, ICSE24 (2002) pp. 11–21. Google ScholarS. Uchitel , J. Kramer and J. Magee , Negative scenarios for implied scenario elicitation, Proc. of FSE (2002) pp. 109–118. Google Scholar-
M. Utting and B. Legeard , Practical Model-based Testing: A tools approach ( Morgan Kaufmann , 2007 ) . Google Scholar M. Veanes , Formal Methods and Testing (2008) pp. 39–76. Crossref, Google ScholarT. Wilke , CTL+ is exponentially more succinct than CTL, Foundations of Software Technology and Theoretical Computer Science (1999) pp. 110–121. Google Scholar
| Remember to check out the Most Cited Articles! |
|---|
|
Check out our titles in C++ Programming! |
