A FRAMEWORK FOR EVALUATING SPECIFICATION METHODS FOR REACTIVE SYSTEMS- EXPERIENCE REPORT

Numerous formal specification methods for reactive systems have been p roposed in the literature. Because the significant differences between the methods are hard to determine, choosing the best method for a par ticular application can be difficult. We have applied several differen t methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL, an d C, to an application problem encountered in the design of software f or AT&T's 5ESS(R) telephone switching system. We have developed a set of criteria for evaluating acid comparing the different specification methods. We argue that the evaluation of a method must take into accou nt not only academic concerns, but also the maturity of the method, it s compatibility with the existing software development process and sys tem execution environment, and its suitability for the chosen applicat ion domain.