Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Especificação Formal
• Técnicas para a especificação não ambígua de
software
• Objectivos
– Explicar o lugar da especificação formal de software no processo de
software
– Explicar quando a utilização de especificação formal é vantajosa d
ponto de vista dos custos
– Descrever o modelo de processo baseado na transformação das
especificações formais num sistema executável
Engenharia de Software
1
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Especificação no Processo de Software
• A especificação e a concepção estão
inextrincavelmente interligados
• A concepção arquitectural é essencial para
estruturar a especificação
• As especificações formais são expressas em notação
matemática com vocabulário definido com precisão,
sintaxe e semânticas
Engenharia de Software
2
1
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Especificação e Concepção
Increasing contractor involvement
Decreasing client involvement
Requirements
definition
Requirements
specification
Architectural
design
Software
specification
High-level
design
Specification
Design
Engenharia de Software
3
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Especificação no Processo de Sofware
Requirements
specification
Formal
specification
Requirements
definition
High-level
design
System
modelling
Engenharia de Software
Architectural
design
4
2
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Especificação Formal em Avaliação
• As técnicas formais não são largamente utilizadas
no desenvolvimento de software à escala industrial
• Dada a relevância da matemática em outras
disciplinas ligadas à engenharia, porquê esta
situação?
Engenharia de Software
5
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
O Porquê da sua não Utilização?
• Conservadorismo inerente da gestão. É difícil de demonstrar
as vantagens da especificação formal de uma forma
objectiva
• Muitos engenheiros não têm treino nas matemáticas
discretas necessárias à especificação formal
• Os clientes do sistema podem ser relutantes em financiar as
actividades de especificação
• Algumas classes de software (particularmente sistemas
interactivos e sistemas concorrentes) são difíceis de
especificar utilizando técnicas correntes
Engenharia de Software
6
3
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
O Porquê da sua não Utilização?
• Há uma ignorância em larga escala da aplicabilidade das
especificações formais
• Há pouco suporte de ferramentas disponíveis para notações
formais
• Alguns cientistas da computação que são familiares com
métodos formais têm falta de conhecimento dos problemas
do mundo real aos quais eles podem ser aplicados e então
empregam a técnica em sistemas não reais, de que não se
encontra aplicabilidade.
Engenharia de Software
7
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Vantagens da Especificação Formal
• Proporciona discernimento nos requisitos de software e sua
concepção
• As especificações formais podem ser analisadas
matematicamente e a consistência e a perfeição aliada à
integralidade da especificação demonstrada. Pode ser
possível provar que a implementação corresponde à
especificação
• As especificações formais podem ser utilizadas para guiar o
pessoal encarregado dos testes dos componentes na
identificação dos casos de teste apropriados
• As especificações formais podem ser processadas utilizando
ferramentas de software. Pode ser possível animar
especificação para proporcionar um protótipo do software
Engenharia de Software
8
4
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Sete mitos do métodos formais
• Software perfeito resulta dos métodos formais
– Sem sentido - a especificação formal é um modelo do mundo real e pode
incorporar incompreensões, erros e omissões. Contudo, uma abordagem formal é
efectiva dado que faz com que os erros de especificação sejam mais fáceis de
detectar e podem constituir uma base não ambígua para concepção do sistema.
• Métodos formais significam proporcionar programas
– Especificar formalmente um sistema é valioso sem verificação formal do
programa dado que força uma análise detalhada prematura no processo de
desenvolvimento
• Métodos formais só podem ser justificados em sistemas onde
a segurança é um factor critico
– A experiência industrial sugere que os custos de desenvolvimento para todas as
classes de sistemas diminuem se for utilizada a especificação formal
Engenharia de Software
9
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Sete mitos do métodos formais
• Métodos formais são para matemáticos
– Sem sentido . Só matemática simples é necessária.
• Métodos formais aumentam os custos de desenvolvimento
– Não provado. Contudo, o padrão de custos é alterado, com mais custo em
fases iniciais do processo de software.
• Os clientes não podem compreender as especificações
formais
– Podem, se as especificações estiverem parafraseadas em linguagem
natural ou por animação de especificações.
• Métodos formais só foram ainda utilizados em sistemas
triviais
– Há agora muitos exemplos publicados de experiências com métodos
formais em sistemas não triviais.
Engenharia de Software
10
5
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
O Veredicto!
• As razões invocadas para a não utilização de métodos e
especificações formais são fracas e de natureza não técnica.
• Contudo, há boas razões para a não utilização desses
métodos, derivadas das alterações havidas no mercado e da
prática em engenharia de software
– A migração para sistemas interactivos. As técnicas de especificação
formal não abrangem de forma efectiva especificação com interface
gráfica
– O sucesso de métodos de engenharia de software no processo de
concepção e desenvolvimento. O investimento em outras técnicas de
engenharia de software pode revelar-se mais vantajosa do ponto de vista
relação custos-proveitos
Engenharia de Software
11
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Utilização dos Métodos Formais
• Estes métodos não deverão ser largamente utilizados num
futuro previsível. De igual forma não se revelarão vantajosos
na relação custos-proveitos para a maioria de classes de
sistemas (ex. sistemas interactivos e de negócio)
• Tornar-se-ão a abordagem normal ao desenvolvimento de
sistemas onde a segurança, fiabilidade sejam críticos e na
definição de standards, eu devem ser não ambíguos e
precisos
• Isto irá alterar o padrão de custos ao longo do processo do
software
Engenharia de Software
12
6
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Custos de Desenvolvimento com Especificação Formal
Cost
Validation
Design and
Implementation
Validation
Design and
Implementation
Specification
Specification
Without formal
specification
With formal
specification
Engenharia de Software
13
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Abordagens de Especificações Formais
• Abordagem algébrica
– O sistema é descrito em termos das operações e os seus relacionamentos
• Abordagem baseada em modelos
– Um modelo para o sistema actua como uma especificação. Este modelo é
construído utilizando entidades matemáticas bem conhecidas tais como
conjuntos e sequências
Engenharia de Software
14
7
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Linguagens de Especificação Formal
Algebraic
Model-based
Sequential
Larch (Guttag et al., 1985) ,
OBJ (Futatsugi et al., 1985)
Z (Spivey, 1989)
VDM (Jones, 1980)
Concurrent
Lotos (Bolognesi and
Brinksma, 1987),
CSP (Hoare, 1985)
Petri Nets (Peterson, 1981)
Engenharia de Software
15
Instituto Superior Politécnico de VISEU
Escola Superior de Tecnologia
Pontos Chave
• A especificação formal do sistema complementa as técnicas informais de
especificação
• As especificações formais são precisas e não ambíguas. Eliminam áreas
de dúvida numa especificação
• A especificação formal força a uma análise dos requisitos do sistema
numa fase prematura. A correcção dos erros nessa fase é mais barato do
que modificar um sistema já entregue
• As técnicas de especificação formal não são vantajosas do ponto de vista
da relação custos-proveitos, no desenvolvimento de sistemas interactivos.
São mais aplicáveis no desenvolvimento de sistemas de segurança crítica
e standards.
Engenharia de Software
16
8