User guidance for creating precise and accessible property specifications

ABSTRACT

Property specifications concisely describe aspects of what a system is supposed to do. No matter what notation is used to describe them, however, it is difficult to represent these properties correctly, since there are often subtle, but important, details that need to be considered. Propel aims to guide users through the process of creating properties that are both accessible and mathematically precise, by providing templates for commonly-occurring property patterns. These templates explicitly represent these subtle details as options. In this paper, we present a new representation of these templates, a Question Tree that asks users a hierarchical sequence of questions about their intended properties. The Question Tree representation is particularly useful for helping users select the appropriate template, but it also complements the finite-state automaton and disciplined natural language representations provided by Propel. We also report on some case studies and on an experimental evaluation of the understandability of the disciplined natural language representation.

REFERENCES

• 1: S. S. Ali. A logical language for natural language processing. In Proc. of the Tenth Biennial Canadian Artificial Intelligence Conf., Banff, Alberta, Canada, May 1994.
• 2: Vincenzo Ambriola , Vincenzo Gervasi, On the Systematic Analysis of Natural Language Requirements with CIRCE, Automated Software Engineering, v.13 n.1, p.107-167, January 2006 [doi>10.1007/s10515-006-5468-2]
• 3: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 4: James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
• 5: Christian Denger , Daniel M. Berry , Erik Kamsties, Higher Quality Requirements Specifications through Natural Language Patterns, Proceedings of the IEEE International Conference on Software-Science, Technology & Engineering, p.80, November 04-05, 2003
• 6: D. Drusinsky. Visual formal specification using (N)TLCharts : Statechart automata with temporal logic and natural language conditioned transitions. In Int. Workshop on Parallel and Distributed Systems: Testing and Debugging, Santa Fe, NM, Apr. 2004.
• 7: M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property specification patterns web site. http://www.cis.ksu.edu/santos/spec-patterns/.
• 8: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 9: Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004 [doi>10.1145/1040291.1040292]
• 10: Norbert E. Fuchs , Uta Schwertel , Rolf Schwitter, Attempto Controlled English - Not Just Another Logic Specification Language, Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation, p.1-20, June 15-19, 1998
• 11: Vincenzo Gervasi , Didar Zowghi, Reasoning about inconsistencies in natural language requirements, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.3, p.277-330, July 2005 [doi>10.1145/1072997.1072999]
• 12: C. L. Heitmeyer. Software Cost Reduction. In J. J. Marciniak, editor, Encyc. of Software Eng. Wiley-Interscience, Jan. 2002.
• 13: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 14: Sascha Konrad , Betty H. C. Cheng, Real-time specification patterns, Proceedings of the 27th international conference on Software engineering, p.372-381, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062526]
• 15: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 16: Mich Luisa , Franch Mariangela , Inverardi Pierluigi, Market research for requirements analysis using linguistic tools, Requirements Engineering, v.9 n.1, p.40-56, February 2004 [doi>10.1007/s00766-003-0179-8]
• 17: O. Mondragon and A. Gates. Supporting elicitation and specification of software properties through patterns and composite propositions. Int. J. of Software Eng. and Knowledge Eng., 14(1):21--41, Feb. 2004.
• 18: O. Mondragon, A. Q. Gates, and O. Sokolsky. Generating properties for runtime monitoring from software specification patterns. Technical Report UTEP-CS-04-21, U. of Texas at El Paso, 2004.
• 19: Margaret H. Smith , Gerard J. Holzmann , Kousha Etessami, Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs, Proceedings of the 5th IEEE International Symposium on Requirements Engineering, p.14-22, August 27-31, 2001
• 20: Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581345]
• 21: Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland [doi>10.1145/336512.336546]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Elicitation methods (e.g., rapid prototyping, interviews, JAD)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools

General Terms:
Design, Verification

Keywords:
property specifications