• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Tesis Doctoral
DOI
10.11606/T.3.2007.tde-03082007-181907
Documento
Autor
Nombre completo
Marcelo Figueiredo Polido
Dirección Electrónica
Instituto/Escuela/Facultad
Área de Conocimiento
Fecha de Defensa
Publicación
São Paulo, 2007
Director
Tribunal
Maruyama, Newton (Presidente)
Cornélio, Márcio Lopes
Cozman, Fabio Gagliardi
Melo, Ana Cristina Vieira de
Rocha, Ricardo Luis de Azevedo da
Título en portugués
Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais.
Palabras clave en portugués
CSP-OZ
Especificação formal
Refinamento de programas
Sistemas de tempo real não crítico
UML-RT
Verificação de modelos
Resumen en portugués
Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho.
Título en inglés
A refinement method for embedded software development: a based UML-RT and formal specification approach.
Palabras clave en inglés
CSP-OZ
Formal specifications
Model validation
Program refinement
Soft real-time systems
UML-RT
Resumen en inglés
In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.
 
ADVERTENCIA - La consulta de este documento queda condicionada a la aceptación de las siguientes condiciones de uso:
Este documento es únicamente para usos privados enmarcados en actividades de investigación y docencia. No se autoriza su reproducción con finalidades de lucro. Esta reserva de derechos afecta tanto los datos del documento como a sus contenidos. En la utilización o cita de partes del documento es obligado indicar el nombre de la persona autora.
abstractedrev.doc (70.50 Kbytes)
DPMRedrev.doc (75.50 Kbytes)
resumoedrev.doc (71.00 Kbytes)
teserevisada.pdf (1.05 Mbytes)
Fecha de Publicación
2007-08-29
 
ADVERTENCIA: Aprenda que son los trabajos derivados haciendo clic aquí.
Todos los derechos de la tesis/disertación pertenecen a los autores
Centro de Informática de São Carlos
Biblioteca Digital de Tesis y Disertaciones de la USP. Copyright © 2001-2022. Todos los derechos reservados.