Specifying reactive systems by abstract events

Description

We consider the problem of specifying reactive systems at different level of abstraction and propose a method for connecting the requirement to the design phase. As in a variety of other approaches, we assume that a process is modelled by a labelled transition system. The requirement phase is supposed to define a class of models, while at the design level, usually via a stepwise refinement, essentially one model is singled out. The connection between the two phases is provided by the notion of abstract event, with its associated specification language. An abstract event is defined as a set of its concrete instances, which are labelled transition sequences and can occur as partial paths over labelled transition trees. Abstract events, which may be non-instantaneous and overlapping, are a flexible tool for expressing abstract requirements and, because of their semantics in term of labelled transition sequences, provide a rather transparent support to the refinement procedure.

Additional details