In this thesis, a design process for reactive systems using \mucharts, a visual formalism that is similar to the specification language Statecharts, is developed. The design process presented here, comprises abstract description of reactive systems, systematic transformation of abstract specifications into detailed specifications, formal verification through model checking, and centralized as well as distributed implementation. All design steps are formally described. For the state-based description of reactive systems, we first define the language \mucharts. \mucharts are a variant of Harel's Statecharts, which, however, avoid the semantic problems and inconsistencies of the latter and are therefore better suited as a basis for distributed implementation of a specification. A formal semantics for \mucharts is developed. While the core language of \mucharts merely consists of three different syntactic constructs, namely sequential automata, a composition operator, and an operator for signal hiding, further syntactic concepts are expressed as syntactic abbreviations. One such example is hierarchical decomposition. The lean core syntax of \mucharts eases the formal definition of all design steps and is a prerequisite for efficient implementation. In order to support a systematic design process, we define a refinement calculus for \mucharts, which builds the basis for transforming abstract behavioral specifications into detailed ones. The soundness of this calculus with respect to the formal semantics is proved. For formal verification of reactive systems, a translation scheme for \mucharts to the formalisms of two well-known model checking tools is given. How to check safety critical properties of a specification is demonstrated exemplarily by means of a running example. A technique that is based on using finite state machines to generate centralized implementations is described. The thesis concludes with an approach for distributed implementation of \onechart specifications. Problems that may occur while constructing a distributed implementation are discussed and appropriate restrictions to avoid non-feasible implementations are made. The semantic equivalence between distributed implementation and original specification is verified.     «

In this thesis, a design process for reactive systems using \mucharts, a visual formalism that is similar to the specification language Statecharts, is developed. The design process presented here, comprises abstract description of reactive systems, systematic transformation of abstract specifications into detailed specifications, formal verification through model checking, and centralized as well as distributed implementation. All design steps are formally described. For the state-based descrip...     »