Mathematics for the exploration of requirements

ABSTRACT

The exploration of requirements is as complex as it is important in ensuring a successful software production and software life cycle. Increasingly, tool-support is available for aiding such explorations. We use a toy example and a case study of modelling and analysing some requirements of the global assembly cache of .NET to illustrate the opportunities and challenges that mathematically founded exploration of requirements brings to the computer science and software engineering curricula.

REFERENCES

• 1: {Clarke00} E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000.
• 2: {Eisenbach03} S. Eisenbach, V. Jurisic, and C. Sadler. Modeling the evolution of .NET programs. In: IFIP International Conference on Formal Methods for Open Distributed Systems, LNCS. Springer Verlag, 2003.
• 3: Donald C. Gause , Gerald M. Weinberg, Exploring Requirements: Quality Before Design, Dorset House Publishing Co., Inc., New York, NY, 1989
• 4: Michael R. A. Huth , Mark Ryan, Logic in computer science: modelling and reasoning about systems, Cambridge University Press, New York, NY, 2000
• 5: Daniel Jackson, Structuring Z specifications with views, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.4, p.365-389, Oct. 1995 [doi>10.1145/226241.226249]
• 6: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 7: Bashar Nuseibeh , Jeff Kramer , Anthony Finkelstein, A Framework for Expressing the Relationships Between Multiple Views in Requirements Specification, IEEE Transactions on Software Engineering, v.20 n.10, p.760-773, October 1994 [doi>10.1109/32.328995]
• 8: David A. Schmidt, The structure of typed programming languages, MIT Press, Cambridge, MA, 1994
• 9: Ian Sommerville , Peter Sawyer , Stephen Viller, Viewpoints for Requirements Elicitation: A Practical Approach, Proceedings of the 3rd International Conference on Requirements Engineering: Putting Requirements Engineering to Practice, p.74-81, April 06-10, 1998
• 10: {Uchitel03} S. Uchitel, R. Chatley, J. Kramer, and J. Magee. LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. In: Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), Lecture Notes in Computer Science, pages 597--601, Warsaw, Poland, 7--11 April 2003. Springer Verlag.

INDEX TERMS

Keywords:
model checking, pragmatics, requirements, under-specification