• 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
 
 
Tese de Doutorado
DOI
10.11606/T.3.2007.tde-03082007-181907
Documento
Autor
Nome completo
Marcelo Figueiredo Polido
E-mail
Unidade da USP
Área do Conhecimento
Data de Defesa
Imprenta
São Paulo, 2007
Orientador
Banca examinadora
Maruyama, Newton (Presidente)
Cornélio, Márcio Lopes
Cozman, Fabio Gagliardi
Melo, Ana Cristina Vieira de
Rocha, Ricardo Luis de Azevedo da
Título em português
Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais.
Palavras-chave em português
CSP-OZ
Especificação formal
Refinamento de programas
Sistemas de tempo real não crítico
UML-RT
Verificação de modelos
Resumo em 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 em inglês
A refinement method for embedded software development: a based UML-RT and formal specification approach.
Palavras-chave em inglês
CSP-OZ
Formal specifications
Model validation
Program refinement
Soft real-time systems
UML-RT
Resumo em 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.
 
AVISO - A consulta a este documento fica condicionada na aceitação das seguintes condições de uso:
Este trabalho é somente para uso privado de atividades de pesquisa e ensino. Não é autorizada sua reprodução para quaisquer fins lucrativos. Esta reserva de direitos abrange a todos os dados do documento bem como seu conteúdo. Na utilização ou citação de partes do documento é obrigatório mencionar nome da pessoa autora do trabalho.
abstractedrev.doc (70.50 Kbytes)
DPMRedrev.doc (75.50 Kbytes)
resumoedrev.doc (71.00 Kbytes)
teserevisada.pdf (1.05 Mbytes)
Data de Publicação
2007-08-29
 
AVISO: Saiba o que são os trabalhos decorrentes clicando aqui.
Todos os direitos da tese/dissertação são de seus autores
Centro de Informática de São Carlos
Biblioteca Digital de Teses e Dissertações da USP. Copyright © 2001-2018. Todos os direitos reservados.