SUPPORTING ELICITATION AND SPECIFICATION OF SOFTWARE PROPERTIES THROUGH PATTERNS AND COMPOSITE PROPOSITIONS
Abstract
Prospec is a tool that assists practitioners in the elicitation and specification of system properties. Practitioners are guided by questions, definitions, and graphics. Prospec introduces the use of composite propositions to identify intended behavior when multiple conditions or events are considered. Multiple conditions or events may represent behavior such as sequences, concurrency, and non-determinism and may define the boundaries of scopes or type of patterns. Prospec is built upon the Specification Pattern System. The tool assists the analyst in making informed decisions about aspects of a specification that may have multiple interpretations. The end product of the tool is a formal specification in Future Interval Logic, Linear Temporal Logic, or Meta Event Definition Language.
References
- , Modeling and Verification of Parallel Processes, ed.
F. Cassez (Springer-Verlag, 2000) pp. 39–57. Google Scholar - IEEE Trans. on Software Engineering 23, 279 (1997). Crossref, ISI, Google Scholar
- K. Moonjoo, M. Viswanathan et al., "Formally specified monitoring of temporal properties", in The 11th Euromicro Conf. on Real-Time Systems, June 1999, pp. 114–122 . Google Scholar
- ACM Computing Surveys 28(4), 626 (1996). Crossref, ISI, Google Scholar
- IEEE Software 11 (1990). Google Scholar
- M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, "Property specification patterns for finite-state verification", in 2nd Workshop on Formal Methods in Software Practice, Florida, USA, March 1998, pp. 7–15 . Google Scholar
- M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, "Patterns in property specification for finite state verification", in 21st Int. Conf. on Software Engineering, CA, USA, May 1999, pp. 411–420 . Google Scholar
- R. Smith, G. Avrunin, L. Clarke, and L. Osterweil, "PROPEL: An approach supporting property elucidation", Proc. Int. Conf. on Software Engineering, Florida, USA, May 2002, pp. 11–21 . Google Scholar
- O. Mondragon, A. Gates, and S. Roach, "Composite propositions: Toward support for formal specification of system properties", in Proc. 27th Annual IEEE/NASA Goddard Software Engineering Workshop, MD, USA, December 2002, pp. 67–74 . Google Scholar
-
E. Gamma , Design Patterns: Elements of Reusable Object-Oriented Software ( Addison-Wesley , California , 1995 ) . Google Scholar - ACM Trans. on Software Engineering and Methodology 3(2), 131 (1994). Crossref, Google Scholar
- , Program Design Calculi,
NATO ASI 118, Series F: Computer and System Sciences , ed.M. Broy (Springer-Verlag, 1993) pp. 287–323. Crossref, Google Scholar - M. H. Smith, G. J. Holzmann, and K. Etessami, "Events and constraints: A graphical editor for capturing logic requirements of programs", in Sixth IEEE Int. Symp. on Requirements Engineering, Toronto, Canada, August 2001, pp. 14–22 . Google Scholar
- O. Mondragon and A. Gates, "Prospec: Support for elicitation and formal specification of software properties", Proc. Runtime Verification Workshop (RV '03), Colorado, USA, July 2003, pp. 67–86 . Google Scholar
- M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan, Electronic Notes in Theoretical Computer Science, eds. K. Havelund and G. Roşu, vol. 55, no. 2 (2001), pp. 97–104, www.elsevier.nl/locate/entc . Google Scholar
- Y. S. RamaKrishna, "Interval logics for temporal specification and verification", Ph.D. Dissertation, Department of Electrical and Computer Engineering, University of California, Santa Barbara, 1993 . Google Scholar
- , High Integrity Software, eds.
V. Winter and S. Kluwer (Academic Press, Boston, 2001) pp. 115–135. Crossref, Google Scholar
| Remember to check out the Most Cited Articles! |
|---|
|
Check out our titles in C++ Programming! |
