Abstract
This paper describes a modeling and verification environment for real-time systems. The environment supports both a graphical design language (Modechart) and a textually based one (Temporal CCS) and implements different methodologies, including simulation, system minimization, and equivalence checking, for analyzing systems. The tool has been applied to the verification of active structural control systems.