Given the complexity of formal specification and analysis for large-scale systems, effective system support in modeling building and in automation of analysis is indispensable to the success of a formal methodology. We have developed a graphics-oriented, Internet-based, and platform-independent formal architectural design, verification and testing environment that helps us to materialize the advantages discussed in the proposal. The system will support graphic-based, interactive, and incremental construction and refinement of complex system models. We will also implement proposed analysis techniques so as to automate the verification process, and experiment with the proposed design-time testing methods and techniques.