A Note on Refinement in Hierarchical Transition Systems
Lüttgen, Gerald (2018): „A Note on Refinement in Hierarchical Transition Systems“. 1. Aufl. Cham: Springer International Publishing doi: 10.1007/978-3-030-00244-2.
Title of the compilation:
Formal Methods for Industrial Critical Systems : 23rd International Conference, FMICS 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings
23rd Intl. Conf. on Formal Methods for Industrial Critical Systems (FMICS 2018)
Year of publication:
Lecture Notes in Computer Science ; 11119
Software engineers frequently employ notations and tools based on transition systems, such as UML state machines and Statecharts, for specifying and reasoning about reactive behaviour. While these notations are typically supported by an operational semantics, they lack a formal underpinning of the incremental refinement practices of engineers who, e.g., place state machines inside states or add outer transitions to states during design. This note sketches how modal transition systems may be applied to formally capture such refinements along state hierarchies, using a hierarchical extension of labelled transition systems that permits engineers to explicitly allow or disallow state refinement and transition extension at each state. A small example testifies to the utility of this framework for hierarchically refining reactive systems.
November 16, 2018