• 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
 
 
Doctoral Thesis
DOI
10.11606/T.3.2007.tde-03082007-181907
Document
Author
Full name
Marcelo Figueiredo Polido
E-mail
Institute/School/College
Knowledge Area
Date of Defense
Published
São Paulo, 2007
Supervisor
Committee
Maruyama, Newton (President)
Cornélio, Márcio Lopes
Cozman, Fabio Gagliardi
Melo, Ana Cristina Vieira de
Rocha, Ricardo Luis de Azevedo da
Title in Portuguese
Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais.
Keywords in Portuguese
CSP-OZ
Especificação formal
Refinamento de programas
Sistemas de tempo real não crítico
UML-RT
Verificação de modelos
Abstract in Portuguese
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.
Title in English
A refinement method for embedded software development: a based UML-RT and formal specification approach.
Keywords in English
CSP-OZ
Formal specifications
Model validation
Program refinement
Soft real-time systems
UML-RT
Abstract in English
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.
 
WARNING - Viewing this document is conditioned on your acceptance of the following terms of use:
This document is only for private use for research and teaching activities. Reproduction for commercial use is forbidden. This rights cover the whole data about this document as well as its contents. Any uses or copies of this document in whole or in part must include the author's name.
abstractedrev.doc (70.50 Kbytes)
DPMRedrev.doc (75.50 Kbytes)
resumoedrev.doc (71.00 Kbytes)
teserevisada.pdf (1.05 Mbytes)
Publishing Date
2007-08-29
 
WARNING: Learn what derived works are clicking here.
All rights of the thesis/dissertation are from the authors
Centro de Informática de São Carlos
Digital Library of Theses and Dissertations of USP. Copyright © 2001-2022. All rights reserved.