Several requirements specification styles for the specification of reactive systems have been proposed in the literature. Informal specifications are the most widely used in the software industry nowadays, mainly because they are "understandable" by domain experts and software engineers, and therefore can be included as part of a software contract. Unfortunately, because of the inherent ambiguity of natural language, these documents are difficult to interpret and maintain. Formal specifications on the other hand, make use of mathematical notations that offer precise syntax and semantics. Unfortunately, because of the complexity of the formal description these documents may not be acceptable to many stakeholders. Visual formalisms bridge the gap between informal and formal specifications by offering graphical notations with semantics. Unfortunately, hand made diagrams become easily unreadable when the requirements complexity increases. In addition, visual formalisms do not enjoy the powerful verification, code optimization, or model-checking techniques that are common to formal notations. 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 [1,3,2] 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 [4] 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.
展开▼
