| Despite spectacular advances in the field of logic-based mathematical analysis the adoption of formal design and validation techniques by the corporate community has been somewhat slow. While accepting in principle the need for formally certified de signs, the common complaint from practitioners has been that formal notations are unintuitive and difficult to use and their analysis time-consuming due to the enormous memory requirements of complex models. This thesis adopts a multi-pronged approach to addressing these grievances. Through unit verification it provides a simple way of analyzing memory-intensive models by extracting that part of the system's behavior that is relevant to the property being proven. Another contribution of the thesis is the design of a formal, hierarchical graphical notation called Architectural Interaction Diagrams (AID) which provides an unique capability of parameterized communication: something other process-algebra based architecture description languages cannot do. Equipped with a rich vocabulary of communication primitives provided as an intrinsic feature of the language, the designer can construct complex, space-efficient simulateable models without having to worry about the mechanisms of inter-model communication. The compositional semantics for Statecharts disallows the user from using interlevel or boundary crossing transitions. This thesis removes this unnatural restriction on design by demonstrating how boundary crossing transitions in Statecharts may be incorporated and compositionality still maintained. |
