The purpose of this work is to combine the advantages of using visual formalisms for the specification of reactive systems with that of using formal verification and program transformation tools developed for textual formalisms. We have developed a tool suite called ViSta that automatically produces statechart layouts based on information extracted from an informal specification. In this paper, we discuss how ViSta is augmented with a tool that automatically translates statecharts to Z specifications. The informal, statechart and Z specifications are inter-related. This ensures consistency between the different representations, and therefore facilitates the verification and validation effort.
展开▼
