Conferencia
Monteverde, D.; Olivero, A.; Yovine, S.; Braberman, V. "VTS-based specification and verification of behavioral properties of AADL models" (2008) 1st International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2008. 503:23-37
Estamos trabajando para incorporar este artículo al repositorio
Consulte la política de Acceso Abierto del editor
Abstract:
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).
Registro:
| Documento: | Conferencia |
| Título: | VTS-based specification and verification of behavioral properties of AADL models |
| Autor: | Monteverde, D.; Olivero, A.; Yovine, S.; Braberman, V. |
| Ciudad: | Toulouse |
| Filiación: | Inst. de Tecnología, UADE, Argentina VERIMAG, CNRS, France Departamento de Computación, FCEyN, UBA, Argentina Conicet, Argentina |
| Palabras clave: | 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 |
| Año: | 2008 |
| Volumen: | 503 |
| Página de inicio: | 23 |
| Página de fin: | 37 |
| Título revista: | 1st International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2008 |
| Título revista abreviado: | CEUR Workshop Proc. |
| ISSN: | 16130073 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde |
Referencias:
- Alfonso, A., Braberman, V., Kicillof, N., Olivero, A., Visual timed event scenarios (2004) Proc. of the 26th ACM/ IEEE ICSE '04, , ACM Press
- Altisen, K., Gossler, G., Pnueli, A., Sifakis, J., Tripakis, S., Yovine, S., A frame-work for scheduler synthesis (1999) Proc. RTSS '99, , IEEE Comp. Soc. Press
- Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F., Fiacre: An intermediate language for model verification in the topcased environment (2008) 4th European Conf. ERTS, , January
- Berthomieu, B., Vernadat, F., Time petri nets analysis with tina (2006) 3rd Int. Conf. on the Quantitative Evaluation of Systems-(QEST'06)
- Berthomieu, B., Vernadat, F., State space abstractions for time petri nets (2007) Handbook of Real-Time and Embedded Systems, Crc Computer & Information Science Series, , Chapman & Hall, July
- Bertrand, D., Déplanche, A.-M., Faucou, S., Roux, O.H., A study of the aadl mode change protocol (2008) 13th IEEE International Conference on Engineering of Complex Computer Systems, , IEEE
- Braberman, V., Kicillof, N., Olivero, A., A scenario-matching approach to the description and model checking of real-time properties (2005) IEEE Transactions on Software Engineering, 31 (12)
- Feiler, P., Hansson, J., Flow latency analysis with the architecture analysis and design language (AADL (2007) Technical Note CMU/SEI-2007-TN-010, , Carnegie Mellon University, June
- Gardey, G., Lime, D., Magnin, M., Roux, O.H., Romeo: A tool for analyzing time petri nets (2005) Computer Aided Verification, pp. 418-423. , Lecture Notes in Computer Science
- Hugues, J., Zalila, B., Pautet, L., Kordon, F., From the prototype to the final embedded system using the ocarina AADL tool suite (2008) ACM Transactions in Embedded Computing Systems, , Oct
- Monteverde, D., (2007) Verificación Automática de Escenarios Condicionales, , Master' thesis, FCEyN Univ. de Buenos Aires
- Monteverde, D., Olivero, A., Yovine, S., Braberman, V., (2008) VTS-based Specification and Verification of Behavioral Properties of AADL Models, , http://www.dc.uba.ar/people/exclusivos/vbraber, Technical report
- (2004) SAE. Architecture Analysis and Design Language, , SAE Standard AS5506
- Singhoff, F., Plantec, A., Dissaux, P., Can we increase the usability of real time scheduling theory? (2008) The Cheddar Project Ada-Europe 2008
- Tripakis, S., Yovine, S., Bouajjani, A., Checking timed buchi automata emptiness efficiently Formal Methods in System Design, 26 (3). , May 200
Citas:
---------- APA ----------
Monteverde, D., Olivero, A., Yovine, S. & Braberman, V. (2008) . VTS-based specification and verification of behavioral properties of AADL models. 1st International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2008, 503, 23-37.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde [ ]
---------- CHICAGO ----------
Monteverde, D., Olivero, A., Yovine, S., Braberman, V. "VTS-based specification and verification of behavioral properties of AADL models" . 1st International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2008 503 (2008) : 23-37.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde [ ]
---------- MLA ----------
Monteverde, D., Olivero, A., Yovine, S., Braberman, V. "VTS-based specification and verification of behavioral properties of AADL models" . 1st International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2008, vol. 503, 2008, pp. 23-37.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde [ ]
---------- VANCOUVER ----------
Monteverde, D., Olivero, A., Yovine, S., Braberman, V. VTS-based specification and verification of behavioral properties of AADL models. CEUR Workshop Proc. 2008;503:23-37.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16130073_v503_n_p23_Monteverde [ ]
