VTS-based specification and verification of behavioral properties of AADL models

AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis o...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Monteverde, D., Olivero, A., Yovine, S., Braberman, V.
Formato:	CONF
Materias:	Behavioral properties Effective translation Model checking tools Model driven design Property specification language Real-time embedded systems Schedulability analysis Specification and verification Model checking Models Petri nets Specification languages Tools Embedded systems
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_16130073_v503_n_p23_Monteverde
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_16130073_v503_n_p23_Monteverde
record_format	dspace
spelling	todo:paper_16130073_v503_n_p23_Monteverde2023-10-03T16:28:09Z VTS-based specification and verification of behavioral properties of AADL models Monteverde, D. Olivero, A. Yovine, S. Braberman, V. Behavioral properties Effective translation Model checking tools Model driven design Property specification language Real-time embedded systems Schedulability analysis Specification and verification Model checking Models Petri nets Specification languages Tools Embedded systems AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (VTS) as a graphical property specification language for AADL, and (2) devises an effective translation from VTS to Time Petri Nets (TPN) which enables model-checking properties expressed in VTS over AADL models using TPN-based tools integrated into AADL-compliant IDEs (e.g., TOPCASED). Fil:Monteverde, D. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_16130073_v503_n_p23_Monteverde
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Behavioral properties Effective translation Model checking tools Model driven design Property specification language Real-time embedded systems Schedulability analysis Specification and verification Model checking Models Petri nets Specification languages Tools Embedded systems
spellingShingle	Behavioral properties Effective translation Model checking tools Model driven design Property specification language Real-time embedded systems Schedulability analysis Specification and verification Model checking Models Petri nets Specification languages Tools Embedded systems Monteverde, D. Olivero, A. Yovine, S. Braberman, V. VTS-based specification and verification of behavioral properties of AADL models
topic_facet	Behavioral properties Effective translation Model checking tools Model driven design Property specification language Real-time embedded systems Schedulability analysis Specification and verification Model checking Models Petri nets Specification languages Tools Embedded systems
description	AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (VTS) as a graphical property specification language for AADL, and (2) devises an effective translation from VTS to Time Petri Nets (TPN) which enables model-checking properties expressed in VTS over AADL models using TPN-based tools integrated into AADL-compliant IDEs (e.g., TOPCASED).
format	CONF
author	Monteverde, D. Olivero, A. Yovine, S. Braberman, V.
author_facet	Monteverde, D. Olivero, A. Yovine, S. Braberman, V.
author_sort	Monteverde, D.
title	VTS-based specification and verification of behavioral properties of AADL models
title_short	VTS-based specification and verification of behavioral properties of AADL models
title_full	VTS-based specification and verification of behavioral properties of AADL models
title_fullStr	VTS-based specification and verification of behavioral properties of AADL models
title_full_unstemmed	VTS-based specification and verification of behavioral properties of AADL models
title_sort	vts-based specification and verification of behavioral properties of aadl models
url	http://hdl.handle.net/20.500.12110/paper_16130073_v503_n_p23_Monteverde
work_keys_str_mv	AT monteverded vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels AT oliveroa vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels AT yovines vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels AT brabermanv vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels
_version_	1782030854960185344

VTS-based specification and verification of behavioral properties of AADL models

Ejemplares similares