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, Daniel, Braberman, Víctor Adrián
Publicado: 2008
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:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde
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 paper:paper_16130073_v503_n_p23_Monteverde
record_format dspace
spelling paper:paper_16130073_v503_n_p23_Monteverde2023-06-08T16:25:18Z VTS-based specification and verification of behavioral properties of AADL models Monteverde, Daniel Braberman, Víctor Adrián 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. 2008 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde 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, Daniel
Braberman, Víctor Adrián
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).
author Monteverde, Daniel
Braberman, Víctor Adrián
author_facet Monteverde, Daniel
Braberman, Víctor Adrián
author_sort Monteverde, Daniel
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
publishDate 2008
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde
http://hdl.handle.net/20.500.12110/paper_16130073_v503_n_p23_Monteverde
work_keys_str_mv AT monteverdedaniel vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels
AT brabermanvictoradrian vtsbasedspecificationandverificationofbehavioralpropertiesofaadlmodels
_version_ 1768545758150131712

Ejemplares similares