This Article 
 Bibliographic References 
 Add to: 
A Framework for Evaluating Specification Methods for Reactive Systems Experience Report
June 1996 (vol. 22 no. 6)
pp. 378-389

Abstract—Numerous formal specification methods for reactive systems have been proposed in the literature. Because the significant differences between the methods are hard to determine, choosing the best method for a particular application can be difficult. We have applied several different methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL, and C, to an application problem encountered in the design of software for AT&T's 5ESS® telephone switching system. We have developed a set of criteria for evaluating and comparing the different specification methods. We argue that the evaluation of a method must take into account not only academic concerns, but also the maturity of the method, its compatibility with the existing software development process and system execution environment, and its suitability for the chosen application domain.

[1] K.E. Martersteck and A.E. Spencer, "Introduction to the 5ESS™Switching System," AT&T Technical J., vol. 64, no. 6, part 2, pp. 1,305-1,314, July-Aug. 1985.
[2] F. Jahanian and A.K. Mok, “Modechart: A Specification Language for Real-Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 10, Oct. 1994.
[3] F. Wagner, "VFSM Executable Specification," Proc. IEEE Int'l Conf. Computer System and Software Engineering, The Hague, pp. 226-231, 1992.
[4] G. Berry and G. Gonthier, "The ESTERELSynchronous Programming Language: Design, Semantics, Implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[5] ISO, LOTOS—A Formal Description Technique Based on the Temporal Ordering of Observational Behavior. ISO, Int'l Standard ISO 8807, 1989.
[6] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, N.J., 1992.
[7] ITU-T, "Specification and Description Language SDL," Recommendation Z.100, 1993.
[8]  S.L. Gerhart, D. Craigen, and T. Ralston, “Experience with Formal Methods in Critical Systems,” IEEE Software, Jan. 1994, pp. 21-28.
[9] C. Lewerentz and T. Lindner, "Case Study 'Production Cell': A Comparative Study in Formal Specification and Verification," technical report, Forschungszentrum Informatik, 1994.
[10] Bellcore, "Synchronous Optical Network (SONET) Transport Systems: Common Generic Criteria," Technical Report TR-NWT-000253, Issue 2, Bellcore, 1991.
[11] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[12] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[13] C. Puchol, D. Stuart, and A.K. Mok, "An Operational Semantics for Modechart Specifications," Technical Report UTCS-TR95-37, Dept. of Computer Sciences, the Univ. of Texas at Austin, Sept. 1995.
[14] P.C. Clements, C.L. Heitmeyer, B.G. Labaw, and A.T. Rose, “MT: A Toolset for Specifying and Analyzing Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., Dec. 1993.
[15] C. Puchol, A.K. Mok, and D. Stuart, "Compiling Modechart Specifications," Proc. IEEE Real-Time Systems Symp., pp. 256-265, Dec. 1995.
[16] "AGEL Workshop Manual Version 3.0," produced by ILOG, Mountain View, Calif., 1989.
[17] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[18] L.J. Jagadeesan, C. Puchol, and J.E. von Olnhausen, “Safety Property Verification of Esterel Programs and Applications to Telecommunications Software,” Proc. Conf. Computer-Aided Verification 1995, Liège, Belgium, July 1995.
[19] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[20] R. Boumezbeur and L. Logrippo, "Specifying Telephone Systems in LOTOS," IEEE Comm. Magazine, vol. 31, no. 8, pp. 38-45, Aug. 1993.
[21] M.A. Ardis, "Lessons from Using Basic Lotos," Sixteenth Int'l Conf. Software Eng.,Sorrento, Italy, pp. 5-14, May 1994.
[22] C.A. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma, "Specification Styles in Distributed Systems Design and Verification," Theoretical Computer Science, vol. 89, pp. 179-206, 1991.
[23] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[24] ITU-T, "Message Sequence Chart," Recommendation Z.120, 1992.
[25] A. Hall, "Using Z as a Specification Calculus for Object-Oriented Systems," VDM and Z—Formal Methods in Software Development, D. Bjørner, C.A.R. Hoare, and H. Langmaack, eds., pp. 290-318. Springer-Verlag, 1990.
[26] P. Zave and M. Jackson, "Where Do Operations Come From? A Multiparadigm Specification Technique," 1994, draft available from the authors.
[27] W.K. Snyder, "The SETL2 Programming Language," technical report, Courant Inst. of Mathematical Sciences, New York Univ., 1990.
[28] J.R. Abrial, The B-Book. Cambridge Univ. Press, 1995.
[29] G.J. Holzmann, “Practical Methods for Formal Validation of SDL Specifications,” Computer Comm., vol. 15, no. 2, pp. 129–134, Mar. 1992.
[30] A.R. Flora-Holmquist, J.D. O'Grady, and M.G. Staskauskas, "Telecommunications Software Design Using Virtual Finite State Machines," Proc. Int'l Switching Symp. (ISS95),Berlin, Apr. 1995.
[31] L.J. Jagadeesan, C. Puchol, and J.E. Von Olnhausen, "A Formal Approach to Reactive Systems Software: A Telecommunications Application in ESTEREL," Formal Methods in System Design, vol. 8, no. 2, Mar. 1996. Preliminary verson appeared in Proc. IEEE Workshop Industrial-Strength Formal Specification Techniques, Apr. 1995.
[32] J. Chaves, "Formal Methods at AT&T, An Industrial Usage Report," Proc. Fourth FORTE Conf. Formal Description Techniques, pp. 83-90,Sydney, Australia, 1991.
[33] P.A. Mataga and P. Zave, "Formal Specification of Telephone Features," Z User Workshop, J.P. Bowen and J.A. Hall, eds., pp. 29-50,Cambridge, Springer-Verlag, 1994.

Index Terms:
Formal methods, specification languages, industrial applications, technology assessment, ESTEREL, LOTOS, Modechart, SDL, VFSM, Z.
Mark A. Ardis, John A. Chaves, Lalita Jategaonkar Jagadeesan, Peter Mataga, Carlos Puchol, Mark G. Staskauskas, James Von Olnhausen, "A Framework for Evaluating Specification Methods for Reactive Systems Experience Report," IEEE Transactions on Software Engineering, vol. 22, no. 6, pp. 378-389, June 1996, doi:10.1109/32.508312
Usage of this product signifies your acceptance of the Terms of Use.