Resumo Especificação Formal Sommerville

Prévia do material em texto

EE2 - Engenharia de Software e Sistemas
Resumo baseado no Livro Engenharia de Software Sommerville e Slides do Professor
Especificação Formal
Apesar de mais de 30 anos de pesquisas em uso de técnicas matemáticas no processo de software, não são usadas em larga escala.
Métodos Formais: 
Especificação formal de sistema
Análise e prova de especificação
Desenvolvimento transformacional
Verificação de programa.
Especificação formal: expressa em linguagem com vocábulos, sintaxe e semântica formalmente definidos Conceitos matemáticos com propriedade bem compreendidas matemática discreta, teoria dos conjuntos, lógica e álgebra.
Pesquisadores apresentaram hipóteses que a especificação formal iria aprimorar a qualidade do software, pois o rigor e analise detalhada levariam a programas com menos erros. Então isso faria com que fosse usada em grande escala no século XXI. Razões principais para a não concretização:
Engenharia de Software bem-sucedida: estruturação de todo o processo de desenvolvimento do projeto e software aprimoraram a qualidade do software.
Mudança de Mercado: Antes a qualidade era o ponto primordial para um software, atualmente é o seu rápido desenvolvimento, o cliente aceita, às vezes, um software com erros se foi entregue rápido. E uma especificação formal é demorada. 
Escopo limitado dos métodos formais: não especificam camadas mais altas do software (interface), o que tem se tornado parte de relativa importância no processo. 
Escalabilidade limitadas dos métodos formais: por serem muito trabalhosos só foram usados de forma bem-sucedida em projetos de pequeno porte.
A especificação formal é uma excelente maneira de descobrir erros da especificação, e apresentá-la de modo não ambíguo. Logo é adequada em uso limitado em parte do núcleo do sistema.
Os métodos formais são usados em desenvolvimento de sistemas críticos, para gerar segurança, confiabilidade e proteção, que são muito importantes nesse tipo de sistema. Como falha nesse tipo de sistema é algo caro, os métodos formais geram uma diminuição de custo.
Especificação formal no processo de software: 
No desenvolvimento de sistemas críticos a especificação formal vem depois da especificação de requisitos do sistema e antes do projeto detalhado do sistema em um desenvolvimento em cascata, que é típico desse tipo de sistema.
Envolvimento do cliente diminui e do fornecedor aumenta à medida que detalhes são acrescentados na especificação. Quanto mais detalhado mais “difícil” do cliente “entender”
Para detalhar a implementação do sistema um linguagem formal pode ser usada para evitar ambigüidade.
O uso de métodos formais aumenta o custo da especificação, mas diminui o da validação, pois menos erros são encontrados.
Duas abordagens usadas para especificação formal:
Uma abordagem algébrica: o sistema é descrito em termos de operações e seus relacionamentos
Uma abordagem baseada em modelos: modelo do sistema é criado por meio de construções matemáticas, como conjuntos e seqüências, e as operações de sistema são definidas em função de como elas modificam seu estado.
Especificação de interface de subsistema
Um sistema grande é dividido em subsistemas, que são desenvolvidos independentemente. 
A especificação de interface é importante, pois subsistemas são projetados para usar serviços de outros subsistemas antes que estes tenham sido implementados. Na especificação é definido quais serviços estarão disponíveis e como serão acessados.
A abordagem algébrica foi inicialmente projetada para definição de interfaces de tipos abstratos de dados, objetos. Já que se concentra nas operações definidas em um objeto.
Especificação de objeto (partes):
Introdução: tipo da entidade especificada, e os imports.
Descrição: Descreve informalmente as operações sobre o tipo
Assinatura: define a sintaxe da interface nomes das operações, seus parâmetros e tipo de resultado
Axiomas: define a semântica de operações pela definição de axiomas que caracterizam o comportamento, as operações para construir as entidades e inspecionar os seus valores
Atividades do processo de desenvolvimento de uma especificação formal:
Estruturação especificação: Definir informalmente as operações associadas a cada classe.
Definição do nome da especificação: um nome para cada tipo abstrato de dados, decidir se eles tem parâmetros genéricos, assim como definir o nome do objeto.
Seleção de operações: escolher operações para cada especificação de acordo com a funcionalidade. Operações para criar instancias do objeto, modificar e inspecionar valores das instâncias.
Especificação informal de operações: descrever de forma informal como cada operação afeta o objeto definido.
Definição de Sintaxe: parte da assinatura da especificação formal.
Definição de axiomas: definir a semântica das operações pela discrição de quais condições são sempre verdadeiras para as diferentes combinações de operações.
Tipos de básicos de operações de um tipo abstrato:
Operações de construtor: criam ou modificam as entidades.
Operações de inspeção: avaliam os atributos da entidade.
Não é necessário construir axiomas para construtores não primitivos, mas pode defini-la usando as operações primitivas de construtor.
Operações são freqüentemente especificadas recursivamente
Especificação de um setor controlado:
Especificação de comportamento:
As técnicas algébricas usadas para descrever interfaces são independentes do estado anterior do objeto, o que é um problema. Uma alternativa é usar a especificação baseada em modelos, que a especificação do sistema é expressa em estados do sistema.
A notação Z é uma técnica madura para especificação baseada em modelos.