Formal framework for communication software

The paper presents a formal specification in the Z/Object-Z notation for a distributed software system. It describes the access switching module that is quite generic and should be widely applicable. The specification emphasizes temporal property within each independent unit and synchronization property between distributed processors in the module. An entire call handling system can be presented by modular object oriented specification using Object-Z notation with temporal constraints. Sequence notation is used for specification of the signal generation and direction in the system. Specification of the system is built up from components, subsystems, conditions and modes that are developed separately-this accounts for behaviors that emerge at the system level