We propose a toolset for designing real-time systems. The toolset is based on a design methodology for real-time systems. The purpose of a design methodology is to provide a set of procedures and guidelines that, with human intervention and interaction, allow designers to systematically obtain implementations of systems that conform precisely to their design specifications. Our methodology is designed for automation. We present the toolset and case study of the design of a simple VCR system. The methodology is based on a formal model and precise descriptions of the components of the system. The underlying model of our methodology is composed of a control level and a data-flow level that, together with a resource scheduler and the application-specific code, make up the system under design.

Testing commercial software is expensive and time consuming.Automated testing methods promise to save a great deal of time and money throughout the software industry.One approach that is well-suited for the reactive systems found in telephone switching systems is specification-based testing.We have built a set of tools to automatically test software applications for violations of safety properties expressed in temporal logic.Our testing system automatically constructs finite state machine oracles corresponding to safety properties, builds test harnesses, and integrates them with the application.The test harness then generates inputs automatically to test the application.We describe a study examining the feasibility of this approach for testing industrial applications.To conduct this study we formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony systems.We then asked a number of computer science graduate students to develop several versions of the APS and use our tools to test them.We found that the tools are very effective, save significant amounts of human effort (at the expense of machine resources), and are easy to use.We also dis-

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.

The Modechart specification language is a formalism for the specification of real-time systems. A toolset for specification, analysis and simulation for Modechart specifications exists for supporting the design and construction of real-time systems. This paper introduces a new tool in the toolset: a compiler for a class of Modechart specifications, namely, that of deterministic system specifications, extended by a subclass of the non-deterministic system specifications. The object code that the compiler generates is in ESTEREL, a member of the synchronous family of programming languages for real-time systems. We discuss a broad approach to the implementation of timing specifications, providing a range of implementation options, from the basic time step unrolling of states in ESTEREL, to the use of system timers. The compiler presented herein allows the specifier to obtain a correct implementation of a Modechart program, including timing constraints.