A Note on Refinement in Hierarchical Transition Systems

Professorship/Faculty: Software Technologies  
Author(s): Lüttgen, Gerald  
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
Pages: 211-222
Edition: 1
ISBN: 978-3-030-00244-2
Series ; Volume: Lecture Notes in Computer Science ; 11119
Language(s): English
DOI: 10.1007/978-3-030-00244-2
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.
Document Type: Conferenceobject
URI: https://fis.uni-bamberg.de/handle/uniba/44799
Release Date: 16. November 2018