 |
Formal description of real-time requirements is a difficult and
error prone task. Conceptual and tool support for this activity
plays a central role in the agenda of technology transference from
the formal verification engineering community to the Real Time
Systems development practice. Here we present VTS,
a visual language to define complex event-based requirements such
as freshness, bounded response, event correlation, etc. The
underlying formalism is based on partial orders and supports
real-time constraints. The problem of checking whether a timed
automaton model of a system satisfies these sort of scenarios is
shown to be decidable. Moreover, we have also developed a tool
that translates visually specified scenarios into observer timed
automata. The resulting automata can be composed with a model
under analysis in order to check satisfaction of the stated
scenarios. We show the benefits of applying these ideas to some
case studies.
|