Title :
Visual timed event scenarios
Author :
Alfonso, A. ; Braberman, V. ; Kicillof, N. ; Olivero, A.
Author_Institution :
Dept. de Computacion, Univ. de Buenos Aires, Argentina
Abstract :
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. In this article 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.
Keywords :
automata theory; formal specification; formal verification; real-time systems; software tools; visual languages; VTS; check satisfaction; conceptual support; event-based requirements; formal description; formal verification; observer timed automata; real-time constraints; real-time requirements; real-time systems development; timed automaton model; tool support; visual language; visual timed event scenarios; Aerospace industry; Application software; Automata; Control systems; Electrical equipment industry; Electronics industry; Embedded system; Formal verification; Logic; Real time systems;
Conference_Titel :
Software Engineering, 2004. ICSE 2004. Proceedings. 26th International Conference on
Print_ISBN :
0-7695-2163-0
DOI :
10.1109/ICSE.2004.1317439