A Note on Refinement in Hierarchical Transition Systems
|Title of the compilation:||Formal Methods for Industrial Critical Systems : 23rd International Conference, FMICS 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings|
|Corporate Body:||23rd Intl. Conf. on Formal Methods for Industrial Critical Systems (FMICS 2018)|
|Publisher Information:||Cham : Springer International Publishing|
|Year of publication:||2018|
|Series ; Volume:||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.
|Release Date:||16. November 2018|