Desenvolvimento de software Cleanroom
Métodos formais foram integrados como uma serie de processos de desenvolvimento de software. Uma abordagem bem documentada que também usa métodos formais é o processo de desenvolvimento Cleanroom. Este processo é uma filosofia de desenvolvimento de software que usa métodos formais para apoiar inspeção rigorosa de software.
O objetivo dessa abordagem é o desenvolvimento de um software com defeito zero. O próprio nome Cleanroom foi uma analogia feita com as unidades de fabricação de semicondutores, onde os defeitos são evitados através de um processo de manufatura em uma atmosfera ultra limpa.
A abordagem Cleanroom, baseia-se nas seguintes estratégias:
- Especificação Formal: o software a ser desenvolvido é especificado formalmente.
- Desenvolvimento Incremental: o software é particionado em incremento desenvolvidos e validados separadamente.
- Programação Estruturada: um número limitado de construções abstratas de controle e de dados são usados. O processo de codificação de um programa é um processo de refinamentos sucessivos da especificação.
- Verificação Estática: o software é verificado estaticamente por meio de inspeções rigorosas de software.
- Testes Estatísticos de Sistema: cada incremento de software e testado estatisticamente parta determinar a confiabilidade. Esses testes são baseados num perfil operacional desenvolvido em paralelo com a especificação do sistema.
O uso desta abordagem tem levado a construção de softwares com poucos erros. Os custos desses projetos foram comparáveis a outros projetos que usaram técnicas de desenvolvimento convencionais.
A inspeção rigorosa do programa e uma parte fundamental do processo Cleanroom. Um modelo de estado do sistema é criado como especificação do sistema, onde o mesmo é refinado através de uma serie de modelos de sistema detalhada para um programa executável.
Os argumentos matemáticos usados nos Cleanroom não são provas formais de correção. Elas dependem do uso do conhecimento de semânticas formais de linguagem de programação para construir teorias que relacionem o programa e a sua especificação formal.
O desenvolvimento Cleanroom funciona quando é praticado por engenheiro habilidosos e comprometido.
Nenhum comentário:
Postar um comentário