| This dissertation deals with the development of methods and tools for the visualization of software requirements for reactive systems. In particular, it attempts to define algorithms whose purposes are to translate information extracted from an informal specification into a graphical notation, namely statecharts, and into a formal notation namely Z.;We have developed a framework for the automatic generation of layouts of statechart diagrams. Our framework is based on several techniques that include hierarchical drawing, labeling, and floorplanning, designed to work in a cooperative environment. The resulting drawings enjoy several important properties: they emphasize the natural hierarchical decomposition of states into substates; they have a low number of edge crossings; they have good aspect ratio; and require a small area.;We have developed a method to translate statecharts to Z specifications. Our method is based on the STATEMATE semantics, and the standard Z notation. We proceed in two steps: first we produce a static Z specification using the concept of state before and state after. Then, we complement this specification with a specification that describes the system's allowable concurrent behavior. |
