Lfm2000 - Fifth NASA Langley Formal Methods Workshop
C. Michael Holloway · NASA Technical Reports Server (NASA) · 2000
This paper introduces the use of abstraction relationships for timed automata. Abstraction relations make it possible to determine when one specification implements another, i.e. when they have the same set of computations. The approach taken herepermits the hiding of internal events and takes into account the timedbehavior of the specification. A new representation of the semantics of a specification is introduced. This representation, min-max automata is morecompact than other types of finite state automata typically usedtorepresent real-time systems, and can beused to define a variety of abstraction relationships. 1 Introduction This paper describes the use of min-max automata to specify the behavior of real-time systems compactly. Originally developed [2] as an alternative representation of timed behavior for the Modechart language[12], in order to support the evaluation of abstraction relationships between Modechart specifications, min-max automata are a general construct for re...