Specification and Verification of Switching Software

This paper describes specification and verification technology for software development. This technology consists of 1) a Specification description language called LAN-S, 2) a compiler to generate data for specification verification, and 3) a specification analysis algorithm (analyzer). A switching system and terminals are regarded as state transition machines in this technology. From specifications described in LAN-S, input data for the specification analyzer are generated. The analyzer incorporates a concept of the reduced reachability tree (RRtree), which can solve the "state space explosion" encountered in the ordinary teachability tree analysis. Using some subprocedure libraries, the switching software specification in LAN-S is transformed into an executable control program for a system with "process based software architecture." When applied to software development for a model switching system SPICE, the analyzer produced a reachability tree smaller than the one produced via the ordinary reachability tree analysis by 99.95 percent, and proved to be applicable to practical systems analysis.