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, A., Braberman, V., Kicillof, N., Olivero, A.
Formato:	CONF
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:	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	todo:paper_02705257_v26_n_p168_Alfonso
record_format	dspace
spelling	todo:paper_02705257_v26_n_p168_Alfonso2023-10-03T15:14:28Z Visual timed event scenarios Alfonso, A. Braberman, V. Kicillof, N. Olivero, A. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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, A. Braberman, V. Kicillof, N. Olivero, A. 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.
format	CONF
author	Alfonso, A. Braberman, V. Kicillof, N. Olivero, A.
author_facet	Alfonso, A. Braberman, V. Kicillof, N. Olivero, A.
author_sort	Alfonso, A.
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
url	http://hdl.handle.net/20.500.12110/paper_02705257_v26_n_p168_Alfonso
work_keys_str_mv	AT alfonsoa visualtimedeventscenarios AT brabermanv visualtimedeventscenarios AT kicillofn visualtimedeventscenarios AT oliveroa visualtimedeventscenarios
_version_	1782029488919412736

Visual timed event scenarios

Ejemplares similares