Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais. / A refinement method for embedded software development: a based UML-RT and formal specification approach.
AUTOR(ES)
Marcelo Figueiredo Polido
DATA DE PUBLICAÇÃO
2007
RESUMO
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.
ASSUNTO(S)
verificação de modelos csp-oz especificação formal uml-rt model validation soft real-time systems uml-rt program refinement formal specifications sistemas de tempo real não crítico refinamento de programas csp-oz
