Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais (2007)
- Authors:
- Autor USP: POLIDO, MARCELO FIGUEIREDO - EP
- Unidade: EP
- Sigla do Departamento: PMR
- Subjects: ESPECIFICAÇÃO DE SISTEMAS E PROGRAMAS; SISTEMAS DE TEMPO-REAL; SISTEMAS EMBUTIDOS; VERIFICAÇÃO E VALIDAÇÃO DE SOFTWARE; UML
- Language: Português
- Abstract: Neste trabalho é apresentado um novo 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 CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a linguagem CSP, que descreve o comportamento de processos concorrentes. A semântica de CSP-OZ é baseada no modelo por falhas e divergências da semântica denotacional, tanto para a parte CSP, quando para a parte Object-Z. É possível utilizar a ferramenta comercial FDR2 através da semântica por falhas e divergências. Porém, como CSPM, a linguagem da ferramenta FDR2, não tem mecanismos para representar características de orientação a objetos, é necessária a tradução das especificações em tipos dados e funções convencionais, descaracterizando a especificação original e, possivelmente gerando erros na especificação para o FDR2. 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 estruturas de dados descritas por Object-Z. Primeiramente, o determinismo existente no diagrama de estados é utilizado, assumindo também que os modelos têm uma semântica bloqueante pode-se utilizar regras simples desimulação ao invés das regras convencionais de simulação forward/backward. Utilizando este resultado, prova-se a equivalência entre método de equivalência de especificações e regras simples de simulação. 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
- Imprenta:
- Data da defesa: 18.05.2007
-
ABNT
POLIDO, Marcelo Figueiredo. Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais. 2007. Tese (Doutorado) – Universidade de São Paulo, São Paulo, 2007. Disponível em: http://www.teses.usp.br/teses/disponiveis/3/3132/tde-03082007-181907/. Acesso em: 13 fev. 2026. -
APA
Polido, M. F. (2007). Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais (Tese (Doutorado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/3/3132/tde-03082007-181907/ -
NLM
Polido MF. Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais [Internet]. 2007 ;[citado 2026 fev. 13 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3132/tde-03082007-181907/ -
Vancouver
Polido MF. Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais [Internet]. 2007 ;[citado 2026 fev. 13 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3132/tde-03082007-181907/
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
