We describe the application of model checking tools to analyze a real-time software challenge in the design of Lucent Technologies' 5ESS telephone switching system.We use two tools: COSPAN for checking real-time properties, and TPWB for checking probabilistic specifications.We report on the feedback given by the tools, and based on our experience, discuss the advantages and the limitations of the approach used.

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.

Numerous formal specification methods for reactive systems have been proposed in the literature.Because the significant differences bet ween 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 o 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.