The Specification of System Components by State Transition Diagrams
Manfred Broy · 2003
This technical memo provides a syntactic and semantic basis for state transition diagrams (STDs) as they are used for the description of state transition machines (STMs) with input and output. STMs serve for the specification of system components. We work with STDs with transition rules labelled by input and output patterns and preand postconditions. We extend our notation to support specifications that deal with the timing of input and output as well. In particular, we work out the following concepts • the semantic model of STMs with input and output, • the semantic model of STDs in terms of predicate logic, • the description of STMs by STDs, • the definition of stream processing functions by STMs, • a syntax for STDs and their labels. In contrast to approaches like statecharts (see [Harel 87]) we rather start from a semantic notion of a STM and then develop a tuned graphical description technique for it. We show also some methodological aspects such as the use of a partitioning of nodes in STDs as a refinement step that leads to STDs with independent transactions for input and output. We briefly discuss hierarchical STDs, time-outs, interrupts, and pre-emption. *) This work was partially sponsored by the Sonderforschungsbereich 342 Werkzeuge und Methoden fur die Nutzung paralleler Rechnerarchitekturen and the industrial research project SysLab sponsored by Siemens Nixdorf and by the DFG under the Leibniz program. Focus FX 2 Mai 30, 1997