This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Making Changes to Formal Specifications: Requirements and an Example
August 1994 (vol. 20 no. 8)
pp. 562-568

Formal methods have had little impact on software engineering practice, despite the fact that most software engineering practitioners readily acknowledge the potential benefits to be gained from the mathematical modeling involved. One reason is that existing modeling techniques tend not to address basic software engineering concerns. In particular, while considerable attention has been paid to the construction of formal models, less attractive maintenance issues have largely been ignored. The purpose of thispaper is to clarify those issues and examine the underlying requirements for change support. The discussion is illustrated with a description of a change technique and tool developed for the formal notation LOTOS. This work was undertaken as part of the SCAFFOLD project, which was concerned with providing broad support for the construction and analysis of formal specifications of concurrent systems. Most of the discussion is applicable to other process-oriented notations such as CCS and CSP.

[1] D. R. Kuhn, "A technique for analyzing the effects of changes in formal specifications,"The Comput. J., vol. 35, pp. 574-578, Dec. 1992.
[2] A. M. L. de Vasconcelos and J. A. McDermid, "Incremental processing ofZspecifications," inFormal Description Techniques V, M. Diaz and R. Groz, Eds. Amsterdam, The Netherlands: North-Holland, 1993, pp. 65-80.
[3] E. Brinksma, "What is the method in formal methods," inFormal Description Techniques IV, K. Parker and G. Rose Eds. Amsterdam, The Netherlands: North-Holland, 1992, pp. 33-50.
[4] J. Woodcock and M. Loomes,Software Engineering Mathematics, New York: Pitman, 1988.
[5] D. W. Bustard, M. T. Norris, R.A. Orr, and A.C. Winstanley, "An exercise in formalising the description of a concurrent system,"Software Practice&Experience, vol. 22, pp. 1069-1098, Dec. 1992.
[6] S. Patel, R. A. Orr, M. T. Norris, and D. W. Bustard, "Tools to support formal methods," inProc. 11th Int. Conf. Software Eng., Pittsburgh, PA, May 1989, pp. 123-132.
[7] D. Whitgift,Methods and Tools for Software Configuration Management, John Wiley, New York, 1991.
[8] I.S.O., "LOTOS--A formal description technique based on the temporal ordering of observational behavior," ISO8807, 1989.
[9] T. Bolognesi and E. Brinksma, "Introduction to the ISO Specification language LOTOS,"Computer Networks ISDN Syst., vol. 14, pp. 25- 59, 1987.
[10] P. H. J. van Eijk, C. A. Vissers, and M. Diaz,The Formal Description Technique LOTOS. Amsterdam, The Netherlands: Elsevier, 1989.
[11] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[12] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[13] D. W. Bustard and M. D. Harrison, "Animating process-oriented specifications: experiences and lessons," inProc. IEE Colloquium Automating Formal Methods for Comput. Assisted Prototyping, London, January 1992.
[14] H. Alexander, "Structuring dialogues using CSP," inFormal Methods in Human-Computer Interaction, M. Harrison and H. Thimbleby, Eds. Cambridge: Cambridge Univ. Press, 1991.
[15] P. H. J. van Eijk and H. Eertink, "Design of the Lotosphere symbolic LOTOS simulator," inFormal Description Techniques III, J. Quemada, J. Mañas, and E. Vazquez Eds. Amsterdam, The Netherlands: North-Holland, 1991, pp. 709-712.
[16] P. H. J. van Eijk, "The Lotosphere Integrated Tool Environment Lite," inFormal Description Techniques IV, K. Parker and G. Rose Eds. Amsterdam, The Netherlands: North-Holland, 1992, pp. 473-476.
[17] A. C. Winstanley and D. W. Bustard: "EXPOSE: An animation tool for process-oriented formal descriptions,"Software Eng., J., vol. 6, pp. 463-475, Nov. 1991.
[18] L. Logrippo, "The University of Ottawa LOTOS toolkit," inFormal Description Techniques III, J. Quemada, J. Mañas, and E. Vazquez Eds Amsterdam, The Netherlands: North-Holland, 1992, pp. 689-692.
[19] G. León, C. D. Kloos, G. González, M. A. Ruz, S. Marchena, L. Santos, and J. Navarro, "ASDE: Design of a transformational environment for LOTOS," inFormal Description Techniques II, S.T. Vuong Ed. Amsterdam, The Netherlands: North-Holland, pp. 501-516, 1990.
[20] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: Prentice-Hall International, 1989.
[21] R. Paige and R. E. Tarjan, "Three Partition Refinement Algorithms,"SIAM J. Computing, vol. 16, pp. 973-989, 1987.
[22] K. G. Larsen, "Context-Dependent bisimulation between processes," Univ. of Edinburgh, Tech. Rep. CST-37-86, 1986.
[23] J. Fernández and L. Mounier, "Verifying bisimulations on the fly," inFormal Description Techniques III, J. Quemada, J. Mañas, and E. Vazquez, Eds. Amsterdam, The Netherlands: North-Holland, 1991, pp. 91-107.
[24] J. C. Fernández, "Aldébaran: A tool for the verification of communicating processes," Tech. Rep. SPECTRE c14, LGI-IMAG, 1989.
[25] T. Bolognesi and M. Caneve, "Squiggles: A tool for the analysis of LOTOS specifications," inFormal Description Techniques, K. J. Turner, Ed. Amsterdam, The Netherlands: North-Holland, 1989, pp. 201-216.
[26] E. Madelaine and D. Vergamini, "Tools for process algebras," inFormal Descriptions Techniques IV, K. Parker and G. Rose, Eds. Amsterdam, The Netherlands: North-Holland, 1992, pp. 463-466.

Index Terms:
formal specification; specification languages; software maintenance; configuration management; formal specifications; software engineering; change technique; tool; formal notation LOTOS; SCAFFOLD project; process-oriented notations; concurrent systems; change control; formal specification; process algebra; LOTOS
Citation:
D.W. Bustard, A.C. Winstanley, "Making Changes to Formal Specifications: Requirements and an Example," IEEE Transactions on Software Engineering, vol. 20, no. 8, pp. 562-568, Aug. 1994, doi:10.1109/32.310666
Usage of this product signifies your acceptance of the Terms of Use.