Partial generation of Java code from Z formal specifications. / Geração parcial de código Java a partir de especificações formais Z.
AUTOR(ES)
Alvaro Heiji Miyazawa
DATA DE PUBLICAÇÃO
2008
RESUMO
Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário.
ASSUNTO(S)
desenvolvimento baseado em modelo formal specification geração de código. software development especificação formal notação z code generation. linguagem java z notation java language model-driven development desenvolvimento de software
Documentos Relacionados
- Proposta de especificação formal em SDL de uma rede de comunicação automotiva baseada no protocolo FlexRay com geração automatica de codigo java
- Métodos formais algébricos para geração de invariantes
- Desenvolvimento de sistemas TINA utilizando a linguagem de especificação formal SDL com geração automatica de codigo Java
- Structural coverage analysis of test sets derived from formal specifications: a comparative study in the space applications context
- Projeto de sistemas de controle multivariáveis robustos com especificações no domínio do tempo.