Deriving operational software specifications from system goals

Abstract

Goal orientation is an increasingly recognized paradigm for eliciting, modeling, specifying and analyzing software requirements. Goals are statements of intent organized in AND/OR refinement structures; they range from high-level, strategic concerns to low-level, technical requirements on the software-to-be and assumptions on its environment. The operationalization of system goals into specifications of software services is a core aspect of the requirements elaboration process for which little systematic and constructive support is available. In particular, most formal methods assume such operational specifications to be given and focus on their a posteriori analysis.The paper considers a formal, constructive approach in which operational software specifications are built incrementally from higher-level goal formulations in a way that guarantees their correctness by construction. The operationalization process is based on formal derivation rules that map goal specifications to specifications of software operations; more specifically, these rules map real-time temporal logic specifications to sets of pre-, post- and trigger conditions. The rules define operationalization patterns that may be used for guiding and documenting the operationalization process while hiding all formal reasoning details; the patterns are formally proved correct once and for all. The catalog of operationalization patterns is structured according to a rich taxonomy of goal specification patterns.Our constructive approach to requirements elaboration requires a multiparadigm specification language that supports incremental reasoning about partial models. The paper also provides a formal semantics for goal operationalization and discusses several semantic features of our language that allow for such incremental reasoning.

References

1. R. J. Back, "A calculus of refinements for program derivation", Acta Informatica, Vol. 25, 1988, 593-624.
2. A. Borgida, J. Mylopoulos and R. Reiter, "And Nothing Else Changes: The Frame Problem in Procedure Specifications", Proc. ICSE'93 - 15th International Conference on Software Engineering, Baltimore, May 1993.
3. E. Borger and R. Gotzhein, "The Light Control Case Study: Problem Description", Journal of Universal Computer Science, Vol. 6 No. 7, 2000.
4. R. W. Butler. An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. NASA Technical Report 110255. NASA Langley Research Center, May 1996.
5. L. Chung, B. Nixon, E. Yu and J. Mylopoulos, Non-functional requirements in software engineering. Kluwer Academic, 2000.
6. A. Dardenne, A. van Lamsweerde and S. Fickas, "Goal-Directed Requirements Acquisition", Science of Computer Programming, Vol. 20, 1993, 3-50.
7. R. Darimont and A. van Lamsweerde, "Formal Refinement Patterns for Goal-Driven Requirements Elaboration", Proc. FSE'4 - Fourth ACM Symp. on the Foundations of Software Engineering, San Francisco, October 1996, 179-190.
8. E. W. Dijkstra, A Discipline of Programming. Prentice-Hall, 1976.
9. M. B. Dwyer, G. S. Avrunin and J. C. Corbett, "Patterns in Property Specifications for Finite-State Verification", Proc. ICSE'99 - 21st Intl. Conference on Software Engineering, Los Angeles, May 1999.
10. J. Fiadeiro and T. Maibaum, "Temporal theories as modularisation units for concurrent system specification", Formal Aspects of Computing, Vol. 4 No.3, 1992, pp. 239-272.
11. S. Fickas and R. Helm, "Knowledge Representation and Reasoning in the Design of Composite Systems", IEEE Trans. on Software Engineering, June 1992, pp. 470-482.
12. M. Fowler, Analysis Patterns - Reusable Object Models. Addison-Wesley, 1997.
13. J. V. Guttag, J. J. Horning, K. D. Jones, S. J. Garland, A. Modet and J. M. Wing. Larch: Languages and tools for formal specification. Springer-Verlag, 1993.
14. D. Harel and A. Naamad, "The STATEMATE Semantics of Statecharts", ACM Trans. Software Eng. and Methodology, Vol. 5 No.4, October 1996, pp. 293-333.
15. C. Heitmeyer, R. Jeffords and B. Labaw, "Automated Consistency Checking of Requirements Specifications", ACM Trans. on Software Engineering and Methodology, Vol. 5 No. 3, July 1996, pp. 231-261.
16. M. Jackson, Software Requirements & Specifications. ACM Press, Addison-Wesley, 1995.
17. D. Jackson, "Structuring Z specifications with views", ACM Transactions on Software Engineering and Methodology, Vol. 4 No. 4, October 1995, 365-389.
18. D. Jackson, "Automating First-Order Relational Logic", Proc. FSE'2000 - ACM SIGSOFT Conf. on Foundations of Software Engineering,. San Diego, November 2000.
19. M. Jackson, Problem Frames - Analyzing and Structuring Software Development Problems. Addison-Wesley, 2001.
20. C. B. Jones. Systematic Software Development Using VDM. 2nd ed., Prentice Hall, 1990.
21. M. Joseph, Real-Time Systems: Specification, Verification and Analysis. Prentice Hall, 1996.
22. R. Koymans, Specifying message passing and time-critical systems with temporal logic, LNCS 651, Springer-Verlag, 1992.
23. J. Kramer, J. Magee, M. Sloman, et al, "CONIC: an Integrated Approach to Distributed Computer Control Systems", IEE Proceedings, Part E 130, 1, January 1983, pp. 1-10.
24. L. Lamport, "The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, Vol. 16 No. 3, May 1994, 872-923.
25. A. van Lamsweerde, R. Darimont and P. Massonet, "Goal-Directed Elaboration of Requirements for a Meeting Scheduler: Problems and Lessons Learned", Proc. RE'95 - 2nd Int. Symp. on Requirements Engineering, York, IEEE, 1995.
26. A. van Lamsweerde, R. Darimont and E. Letier, "Managing Conflicts in Goal-driven Requirements Engineering", IEEE Transactions on Software Engineering, Vol. 24, No. 11, Nov. 1998, pp.908-926.
27. A. van Lamsweerde and L. Willemet, "Inferring Declarative Requirements Specifications from Operational Scenarios", IEEE Trans. on Sofware. Engineering, Special Issue on Scenario Management, Dec. 1998, pp. 1089-1114.
28. A. van Lamsweerde and E. Letier, "Handling Obstacles in Goal-Oriented Requirements Engineering", IEEE Transactions on Software Engineering, Special Issue on Exception Handling, October 2000.
29. A. van Lamsweerde, "Requirements Engineering in the Year 00: A Research Perspective". Invited Keynote Paper, Proc. ICSE'2000: 22nd International Conference on Software Engineering, ACM Press, 2000, pp. 5-19.
30. A. van Lamsweerde, "Formal Specification: a Roadmap". In The Future of Software Engineering, A. Finkelstein (ed.), ACM Press, 2000, pp. 147-160.
31. A. van Lamsweerde, "Goal-Oriented Requirements Engineering: A Guided Tour". Invited minitutorial, Proc. RE'O1 - International Joint Conference on Requirements Engineering, Toronto, IEEE, August 2001, pp.249-263.
32. E. Letier, Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph.D. Thesis, University of Louvain, May 2001; http://www.info.ucl.ac.be/people/eletier/thesis.html.
33. E. Letier and A. van Lamsweerde, "Agent-Based Tactics for Goal-Oriented Requirements Elaboration", Proc. ICSE'02 - 24th Intl. Conf. on Software Engineering, Orlando, IEEE CS Press, May 2002.
34. Y. Maibaum, "Temporal Reasoning over Deontic Specifications," in J. Ch. Meyer and R. J. Wieringa (Eds.), Deontic Logic in Computer Science - Normative System Specification, Wiley, 1993, pp. 141-202.
35. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992.
36. Z. Manna and the STep Group, "STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems", Proc. CAV'96 - 8th Intl. Conf. on Computer-Aided Verification, LNCS 1102, Springer-Verlag, July 1996, pp. 415-418.
37. P. Massonet and A. van Lamsweerde, "Analogical Reuse of Requirements Frameworks", Proc. RE-97 - 3rd Int. Symp. on Requirements Engineering, Annapolis, 1997, 26-37.
38. C. C. Morgan, Programming from Specifications, 2nd Edition, Prentice-Hall, 1994.
39. D. L. Parnas and J. Madey, "Functional Documents for Computer Systems", Science of Computer Programming, Vol. 25, 1995, pp. 41-61.
40. B. Potter, J. Sinclair and D. Till. An introduction to formal specification and Z. Prentice Hall, 1991.
41. P. Zave and M. Jackson, "Four dark corners of requirements engineering", ACM Trans. Software Eng. and Methodology, Vol. 6 No. 1, January 1997, pp. 1-30.

Index Terms

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Correctness

      • Formal methods

• Theory of computation

  • Logic

    • Proof theory