A Z-based approach to specifying and analyzing complex systems

The difficult task of developing safety-critical systems requires the use of methods and tools that allow developers to manage inherent complexity and to meticulously specify, implement, and analyze desired behavior. Development environments based on formal specification techniques supported by CASE tools can facilitate quality development of such systems. We present our proposed environment for the development of high-assurance systems. The environment provides CASE support for developing and analyzing graphical and formal representations of system structure and behavior. We illustrate the use of the environment with a traffic control system