State-Based Modeling (Automata)

Summary of Most Relevant Topic Papers

Today, we see that many informatics theories are based on state machines in various forms, including Petri Nets or temporal logics. Moreover, software engineering is particularly interested in using state machines for modeling systems.

Nonetheless, we believe that a sound and precise integration of the digital theory (automata) of informatics with control theory (calculus) used by almost all other engineering and science disciplines is one of the most interesting challenges we experience now. Moreover, cyber-physical systems (CPS) (see Cyber Physical Systems (CPS)) urgently require such an integrated theory.

Our contributions to state-based modeling can be split into three parts:

  1. Understanding how to model object-oriented and distributed software using state machines, respectively, Statecharts.
  2. Understanding refinement and composition on state machines.
  3. Applying state machines for modeling of systems.

State Machines as Semantics for Object-Oriented Distributed Software

A practically usable language for state-based modeling must be different from the pure theory because a concrete modeling notation, for example, allows us to denote finitely many (typically very few) states only, while the underlying theory usually has an infinite state space.

In early publications, such as [GKR96], we have discussed how a system model can describe object-oriented systems. We then build onto these experiences to create a complete semantic model for object-oriented systems in [BCR07b]. Objects, inheritance, states, method calls, stack, distribution, time as well as synchronous and asynchronous communication are completely defined and encoded into state machines. The theory is, therefore, suitable as a semantic model for any kind of discrete system. Hence, [BCGR09a] describes a condensed version of this system model and [BCGR09] discusses design decisions and how to use the system model for denotational semantics – and taming the complexity of the system model.

Refinement and Refactoring of State Machines

Starting with [PR94], we investigated how to use state machines to describe the abstract behavior of superclasses and refine it in subclasses. While the description in [PR94] ist relatively informal, we have formalized the refinement relation in [RK96] by mapping a state machine to a set of possible component behaviors based on the streams of the Focus (see Modeling Software Architecture) theory. In [Rum96], we provide constructive transformation rules for refining automata behavior and prove their correctness. This theory is applied to features in [KPR97], where a feature is a sub-automaton that adapts the original behavior in a refining form, precisely clarifying where feature interaction is allowed or harmful.

It became apparent that a state machine either serves as an implementation, where the described behavior is partial and can only be extended but not adapted, or that a state machine describes a specification, where the behavior is constrained to a possible, underspecified set of reactions, promised to the external users of a state machine. Here, refinement always means the reduction of underspecification, telling more behavioral details to the external user. This is constructively achieved, e.g., by removing transitions that have alternatives or adding new behavior (transitions) in cases where previously no transition was applicab.

Specification languages are particularly strong if only explicitly given statements, and no additional implicit assumptions, hold (such as implicitly ignoring messages if a transition cannot process them) as detailed in [Rum96] and [Rum16]. The concept of chaos completion should be used to define the semantics of incomplete state machines. This is much better suited for behavioral refinements than the concept of ignoring messages or error handling in cases where no explicit transition is given. The main disadvantage of “implicit ignoring” is that you never know whether the specifier intended this as desired behavior or just did not care – which is a big difference when aiming to refine the specifier’s model.

Our State Machine Formalism: I/Oω Automata

[Rum96] describes an I/Oω-automaton as (S, Min, Mout, δ, I) consisting of:

  • states S
  • input messages Min
  • output messages Mout
  • transition relation δ ⊆ S x Min x S x Moutω;
  • initial states I

where Moutω = Moutω ∪ Mout∞ is the set of all finite and infinite words over Mout.

Transition relation δ is nondeterministic and incomplete. Each transition has one single input message from Min but an arbitrary long sequence of output messages from Mout. Nondeterminism is handled as underspecification allowing the implementation (or the developer) to choose. Incompleteness is also understood as underspecification allowing arbitrary (chaotic) behavior, assuming that a later implementation or code generator will choose a meaningful implementation. Still, a specifier does not have to decide up-front. Fairness of choice for transitions is not assumed (but possible), as it is counterproductive to refinement by deciding on one alternative during the implementation process.

Most interestingly, describing transitions in δ with input and corresponding output leads to a much more abstract form of state machines, which can actually be used in the modeling process. First, no (explicit) intermediate states are necessary to distribute a sequence of output messages in individual transitions (which is the case in classic Lynch/Tuttle I/O-automata, where a transition has exactly one input or output message). Second, our I/Oω automata preserve the causal relation between input and output on the transitions (whereas I/O automata distribute this over many transitions). We believe I/Oω automata are therefore suited as a human modeling language and are thus used in a syntactically enriched, comfortable form as Statecharts in [Rum16] (https://www.mbse.se-rwth.de/) and [Rum17] (https://www.mbse.se-rwth.de/).

Composition of State Machines

One state machine describes one component. In a distributed system, many state machines are necessary to describe collaborating components. The overall behavior of the component collaboration must then be derivable from the knowledge about the form of composition (architecture describing communication channels) and the specified behavior (state machines) of the components. [GR95] describes how timed state machines are composed.

This technique is embedded in the composition and behavioral specifications concepts of Focus using streams and state machines in a compact overview article [BR07]. Most important, refinement of a component behavior by definition leads to a refinement of the composed system. This is a very important property, which is unfortunately not present in many other approaches, where system integration is a nightmare when components evolve.

Unfortunately, the untimed, event-driven version of state machines that is very well suited for refinement and abstract specification has no composition in general. Further investigation is necessary.

Usage of Automata-based Specification

All our knowledge about state machines is being embedded in the model-based development method for the UML in [Rum16] and [Rum17]. Furthermore, we applied it to robotics (see also Robotics Architectures and Tasks) with the MontiArcAutomaton infrastructure ([RRW14a], [RRW13], see also Modeling Software Architecture), for Cyber-Physical Systems in [RW18], in a modeling language combining state machines and an architectural description language in [THR+13] as well as in building management systems in [FLP+11b].

Key Statements

  1. I/Oω automata (state machines) can be used for I/O-specification of components, objects, agents.
  2. Semantics of finitely depictable state machine models can be mapped to infinite behavior implementations.
  3. Nondeterminism of the state machine is interpreted as underspecification of the model and can be refined in the development process as well as inherited to subclasses.
  4. Refinement of state machines is described as set of constructively applicable transformations (refactoring techniques).
  5. A sound semantics for a state machine is given by a mapping to Focus streams that is compatible with refinement and composition.

Selected Topic-Specific Publications

  1. [RW18]
    B. Rumpe, A. Wortmann:
    Abstraction and Refinement in Hierarchically Decomposable and Underspecified CPS-Architectures.
    In: Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday, Lohstroh, Marten and Derler, Patricia Sirjani, Marjan (Eds.), pp. 383-406, LNCS 10760, ISBN 978-3-319-95246-8, Springer, 2018.
  2. [Rum17]
    B. Rumpe:
    Agile Modeling with UML: Code Generation, Testing, Refactoring.
    Springer International, May 2017.
  3. [Rum16]
    B. Rumpe:
    Modeling with UML: Language, Concepts, Methods.
    Springer International, Jul. 2016.
  4. [RRW14a]
    J. O. Ringert, B. Rumpe, A. Wortmann:
    Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton.
    Aachener Informatik-Berichte, Software Engineering, Band 20, Shaker Verlag, Dec. 2014.
  5. [THR+13]
    U. Thomas, G. Hirzinger, B. Rumpe, C. Schulze, A. Wortmann:
    A New Skill Based Robot Programming Language Using UML/P Statecharts.
    In: Conference on Robotics and Automation (ICRA’13), pp. 461-466, IEEE, 2013.
  6. [RRW13]
    J. O. Ringert, B. Rumpe, A. Wortmann:
    From Software Architecture Structure and Behavior Modeling to Implementations of Cyber-Physical Systems.
    In: Software Engineering Workshopband (SE’13), Volume 215, pp. 155-170, LNI, 2013.
  7. [FLP+11b]
    M. N. Fisch, M. Look, C. Pinkernell, S. Plesser, B. Rumpe:
    State-based Modeling of Buildings and Facilities.
    In: Enhanced Building Operations Conference (ICEBO’11), 2011.
  8. [BCGR09a]
    M. Broy, M. V. Cengarle, H. Grönniger, B. Rumpe:
    Definition of the UML System Model.
    In: UML 2 Semantics and Applications, K. Lano (Eds.), pp. 63-93, ISBN 978-0-470-52261-5, John Wiley & Sons, Nov. 2009.
  9. [BCGR09]
    M. Broy, M. V. Cengarle, H. Grönniger, B. Rumpe:
    Considerations and Rationale for a UML System Model.
    In: UML 2 Semantics and Applications, K. Lano (Eds.), pp. 43-61, ISBN 978-0-470-52261-5, John Wiley & Sons, Nov. 2009.
  10. [BR07]
    M. Broy, B. Rumpe:
    Modulare hierarchische Modellierung als Grundlage der Software- und Systementwicklung.
    In: Informatik-Spektrum, Band 30(1), pp. 3-18, Springer Berlin, Feb. 2007.
  11. [BCR07b]
    M. Broy, M. V. Cengarle, B. Rumpe:
    Towards a System Model for UML. Part 3: The State Machine Model.
    TU Munich, TUM-I0711, Technical Report, Germany, Feb. 2007.
  12. [KPR97]
    C. Klein, C. Prehofer, B. Rumpe:
    Feature Specification and Refinement with State Transition Diagrams.
    In: Workshop on Feature Interactions in Telecommunications Networks and Distributed Systems, pp. 284-297, ISBN 90-5199-347-1, IOS-Press, 1997.
  13. [GKR96]
    R. Grosu, C. Klein, B. Rumpe:
    Enhancing the SysLab System Model with State.
    TU Munich, TUM-I9631, Technical Report, Germany, Jul. 1996.
  14. [Rum96]
    B. Rumpe:
    Formale Methodik des Entwurfs verteilter objektorientierter Systeme.
    ISBN 3-89675-149-2, Herbert Utz Verlag Wissenschaft, München, Deutschland, 1996.
  15. [RK96]
    B. Rumpe, C. Klein:
    Automata Describing Object Behavior.
    In: Object-Oriented Behavioral Specifications, B. Harvey, H. Kilov (Eds.), pp. 265-286, Kluwer Academic Publishers, 1996.
  16. [GR95]
    R. Grosu, B. Rumpe:
    Concurrent Timed Port Automata.
    TU Munich, TUM-I9533, Technical Report, Germany, Oct. 1995.
  17. [PR94]
    B. Paech, B. Rumpe:
    A new Concept of Refinement used for Behaviour Modelling with Automata.
    In: Proceedings of the Industrial Benefit of Formal Methods (FME’94), pp. 154-174, LNCS 873, Springer, 1994.