Visual timed event scenarios

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 arti...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Alfonso, Alejandra, Braberman, Víctor Adrián, Kicillof, Nicolás
Publicado:	2004
Materias:	Automata theory Computer aided analysis Computer programming languages Constraint theory Embedded systems Real time systems Systems engineering Computer aided verification techniques Safety critical systems Timed automaton model VTS Software engineering
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v26_n_p168_Alfonso http://hdl.handle.net/20.500.12110/paper_02705257_v26_n_p168_Alfonso
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_02705257_v26_n_p168_Alfonso
record_format	dspace
spelling	paper:paper_02705257_v26_n_p168_Alfonso2023-06-08T15:24:37Z Visual timed event scenarios Alfonso, Alejandra Braberman, Víctor Adrián Kicillof, Nicolás Automata theory Computer aided analysis Computer programming languages Constraint theory Embedded systems Real time systems Systems engineering Computer aided verification techniques Safety critical systems Timed automaton model VTS Software engineering 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. Fil:Alfonso, A. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Kicillof, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2004 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v26_n_p168_Alfonso http://hdl.handle.net/20.500.12110/paper_02705257_v26_n_p168_Alfonso
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Automata theory Computer aided analysis Computer programming languages Constraint theory Embedded systems Real time systems Systems engineering Computer aided verification techniques Safety critical systems Timed automaton model VTS Software engineering
spellingShingle	Automata theory Computer aided analysis Computer programming languages Constraint theory Embedded systems Real time systems Systems engineering Computer aided verification techniques Safety critical systems Timed automaton model VTS Software engineering Alfonso, Alejandra Braberman, Víctor Adrián Kicillof, Nicolás Visual timed event scenarios
topic_facet	Automata theory Computer aided analysis Computer programming languages Constraint theory Embedded systems Real time systems Systems engineering Computer aided verification techniques Safety critical systems Timed automaton model VTS Software engineering
description	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.
author	Alfonso, Alejandra Braberman, Víctor Adrián Kicillof, Nicolás
author_facet	Alfonso, Alejandra Braberman, Víctor Adrián Kicillof, Nicolás
author_sort	Alfonso, Alejandra
title	Visual timed event scenarios
title_short	Visual timed event scenarios
title_full	Visual timed event scenarios
title_fullStr	Visual timed event scenarios
title_full_unstemmed	Visual timed event scenarios
title_sort	visual timed event scenarios
publishDate	2004
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v26_n_p168_Alfonso http://hdl.handle.net/20.500.12110/paper_02705257_v26_n_p168_Alfonso
work_keys_str_mv	AT alfonsoalejandra visualtimedeventscenarios AT brabermanvictoradrian visualtimedeventscenarios AT kicillofnicolas visualtimedeventscenarios
_version_	1768543132852420608

Visual timed event scenarios

Ejemplares similares