Please use this identifier to cite or link to this item: https://repositorio.ufba.br/handle/ri/13470
metadata.dc.type: Artigo de Periódico
Title: Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems
Other Titles: Innovations in Systems and Software Engineering
Authors: Muniz, André Luís Nunes
Andrade, Aline Maria Santos
Lima, George Marconi de Araújo
metadata.dc.creator: Muniz, André Luís Nunes
Andrade, Aline Maria Santos
Lima, George Marconi de Araújo
Abstract: A new tool for integrating formal methods, particularly model checking, in the development process of component-based real-time systems specified in UML is proposed. The described tool, TANGRAM (Tool for Analysis of Diagrams), performs automatic translation from UML diagrams into timed automata, which can be verified by the UPPAAL model checker. We focus on the CORBA Component Model. We demonstrate the overall process of our approach, from system design to verification, using a simple but real application, used in train control systems. Also, a more complex case study regarding train control systems is described.
Keywords: Components
UML
Real-time systems
Model checking
UPPAAL
metadata.dc.rights: Acesso Aberto
URI: http://repositorio.ufba.br/ri/handle/ri/13470
Issue Date: 2010
Appears in Collections:Artigo Publicado em Periódico (PPGM)

Files in This Item:
File Description SizeFormat 
10.1007_s11334-009-0103-6.pdf500,11 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.