This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Where Do Operations Come From? A Multiparadigm Specification Technique
July 1996 (vol. 22 no. 7)
pp. 508-528

Abstract—We propose a technique to help people organize and write complex specifications, exploiting the best features of several different specification languages. Z is supplemented, primarily with automata and grammars, to provide a rigorous and systematic mapping from input stimuli to convenient operations and arguments for the Z specification. Consistency analysis of the resulting specificaiton is based on the structural rules. The technique is illustrated by two examples, a graphical human-computer interface and a telecommunications system.

[1] G.D. Abowd and A.J. Dix, "Integrating Status and Event Phenomena in Formal Specifications of Interacting Systems, Proc. Second ACM SIGSOFT Symp. Foundations of Software Engineering, pp. 44-52, ACM Press, ISBN 0-89791-691-3, 1994.
[2] R. Boumezbeur and L. Logrippo, "Specifying Telephone Systems in LOTOS," IEEE Comm. Magazine, vol. 31, no. 8, pp. 38-45, Aug. 1993.
[3] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[4] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[5] D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman, "On the Formal Semantics of Statecharts," Proc. Second IEEE Symp. Logic in Computer Science, pp. 54-64,Ithaca, New York, 1987.
[6] D. Harel, H. Lachover, A. Naamad, A. Pnuelli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, "Statemate: A Working Environment for the Development of Complex Reactive Systems," IEEE Trans. Software Eng., vol. 16, no. 4, pp. 403-414, Apr. 1990.
[7] H.R. Hartson and D. Hix, "Human-Computer Interface Management: Concepts and Systems for Its Management," ACM Computing Surveys, vol. 21, no, 1, pp. 5-92, Mar. 1989.
[8] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[9] International Organization for Standardization, "LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behavior, ISO 8807, 1989.
[10] D. Jackson, "Structuring Z Specifications with Views, ACM Trans. on Software Engineering and Methodology, vol. 4, no. 4, pp. 365-389, Oct. 1995.
[11] M.A. Jackson, Principles of Program Design. Academic Press, 1975.
[12] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[13] A. Kay and J.N. Reed, "A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange," IEEE Trans. Software Engineering, vol. 19, no. 6, pp. 625-639, June 1993.
[14] P. Mataga and P. Zave, "A Formal Specification of Some Important 5ESS®Features, Part III: Connections and Provisioning," AT&T Bell Laboratories Tech Memo., Murray Hill, N.J., Oct. 1993.
[15] P. Mataga and P. Zave, "Formal Specification of Telephone Features, Proc. Eighth Z User Meeting, pp. 29-50. Springer-Verlag, ISBN 3-540-19884-9, 1994.
[16] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[17] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[18] A. Pnueli and M. Shalev, "What is in a Step?: On the Semantics of Statecharts," J. Klop, J. Meijer, and J. Rutten, eds., J.W. de Baker, Liber Amicorum, pp. 373-400. CWI, Amsterdam, 1989.
[19] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, N.J., 1992.
[20] J. Woodcock and M. Loomes, Software Engineering Mathematics: Formal Methods Demystified.London: Pitman Publishing, 1988.
[21] P. Zave and D. Jackson, "Practical Specification Techniques for Control-Oriented Systems. G.X. Ritter, ed., Information Processing '89, Proc. IFIP 11th World Computer Congress, pp. 83-88. North-Holland, ISBN 0-444-88015-1, 1989.
[22] P. Zave and M. Jackson, "Conjunction as Composition," ACM Trans. Software Engineering and Methodology, vol. 2, no. 4, pp. 379-411, Oct. 1993.
[23] P. Zave and P. Mataga, "A Formal Specification of Some Important 5ESS®Features, Part I: Overview," AT&T Bell Laboratories Tech Memo., Murray Hill, N.J., Oct. 1993.
[24] P. Zave and P. Mataga, "A Formal Specification of Some Important 5ESS®Features, Part II: Telephone States and Digit Analysis. AT&T Bell Laboratories Tech Memo., Murray Hill, N.J., Oct. 1993.

Index Terms:
Formal methods, multiparadigm specification, consistency analysis, telecommunications, graphical human-computer interfaces, Z.
Citation:
Pamela Zave, Michael Jackson, "Where Do Operations Come From? A Multiparadigm Specification Technique," IEEE Transactions on Software Engineering, vol. 22, no. 7, pp. 508-528, July 1996, doi:10.1109/32.538607
Usage of this product signifies your acceptance of the Terms of Use.