Especificação formal

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

Em ciência da computação , especificações formais são técnicas baseadas matematicamente cujo objetivo é ajudar na implementação de sistemas e softwares. Eles são usados ​​para descrever um sistema, analisar seu comportamento e auxiliar em seu projeto, verificando as principais propriedades de interesse por meio de ferramentas de raciocínio rigorosas e eficazes. [1] [2] Essas especificações são formais no sentido de que possuem uma sintaxe, sua semântica está dentro de um domínio e podem ser usadas para inferir informações úteis. [3]

Motivação

A cada década que passa, os sistemas computacionais se tornam cada vez mais poderosos e, consequentemente, mais impactantes para a sociedade. Devido a isso, melhores técnicas são necessárias para auxiliar no projeto e implementação de software confiável. As disciplinas de engenharia estabelecidas usam a análise matemática como base para criar e validar o design do produto. As especificações formais são uma maneira de alcançar isso na confiabilidade da engenharia de software, como já foi previsto. Outros métodos, como testes , são mais comumente usados ​​para melhorar a qualidade do código. [1]

Usa

Dada tal especificação , é possível usar técnicas de verificação formal para demonstrar que um projeto de sistema está correto em relação à sua especificação. Isso permite que projetos de sistema incorretos sejam revisados ​​antes que grandes investimentos sejam feitos em uma implementação real. Outra abordagem é usar etapas de refinamento provavelmente corretas para transformar uma especificação em um projeto, que é finalmente transformado em uma implementação correta por construção .

É importante notar que uma especificação formal não é uma implementação, mas pode ser usada para desenvolver uma implementação . As especificações formais descrevem o que um sistema deve fazer, não como o sistema deve fazê-lo.

Uma boa especificação deve ter alguns dos seguintes atributos: adequada, internamente consistente, não ambígua, completa, satisfeita, mínima [3]

Uma boa especificação terá: [3]

  • Construtibilidade, gerenciabilidade e evolução
  • Usabilidade
  • Comunicabilidade
  • Análise poderosa e eficiente

Uma das principais razões pelas quais há interesse em especificações formais é que elas fornecerão a capacidade de realizar provas em implementações de software. [2] Essas provas podem ser usadas para validar uma especificação, verificar a exatidão do projeto ou provar que um programa satisfaz uma especificação. [2]

Limitações

Um design (ou implementação) nunca pode ser declarado “correto” por si só. Ela só pode ser “correta em relação a uma determinada especificação”. Se a especificação formal descreve corretamente o problema a ser resolvido é uma questão separada. Também é uma questão difícil de abordar, uma vez que, em última análise, diz respeito ao problema de construir representações formais abstratas de um domínio de problema concreto informal , e tal etapa de abstração não é passível de prova formal. No entanto, é possível validar uma especificação provando teoremas de “desafio”relativas às propriedades que se espera que a especificação exiba. Se corretos, esses teoremas reforçam a compreensão do especificador da especificação e sua relação com o domínio do problema subjacente. Caso contrário, a especificação provavelmente precisa ser alterada para refletir melhor a compreensão do domínio dos envolvidos na produção (e implementação) da especificação.

Métodos formais de desenvolvimento de software não são amplamente utilizados na indústria. A maioria das empresas não considera rentável aplicá-los em seus processos de desenvolvimento de software. [4] Isso pode ocorrer por vários motivos, alguns dos quais são:

  • Tempo
    • Alto custo inicial inicial com baixos retornos mensuráveis
  • Flexibilidade
    • Muitas empresas de software usam metodologias ágeis que focam na flexibilidade. Fazer uma especificação formal de todo o sistema com antecedência é muitas vezes percebido como o oposto de flexível. No entanto, existem algumas pesquisas sobre os benefícios do uso de especificações formais com desenvolvimento "ágil" [5]
  • Complexidade
    • Eles exigem um alto nível de conhecimento matemático e habilidades analíticas para entendê-los e aplicá-los efetivamente [5]
    • Uma solução para isso seria desenvolver ferramentas e modelos que permitam implementar essas técnicas, mas ocultar a matemática subjacente [2] [5]
  • Escopo limitado [3]
    • Eles não capturam propriedades de interesse para todas as partes interessadas no projeto [3]
    • Eles não fazem um bom trabalho de especificação de interfaces de usuário e interação do usuário [4]
  • Não é rentável
    • Isso não é totalmente verdade, limitando seu uso apenas a partes essenciais de sistemas críticos, eles mostraram ser econômicos [4]

Outras limitações: [3]

Paradigmas

As técnicas de especificação formal existem em vários domínios e em várias escalas há algum tempo. [6] As implementações de especificações formais diferem dependendo do tipo de sistema que estão tentando modelar, como são aplicadas e em que ponto do ciclo de vida do software foram introduzidas. [2] Esses tipos de modelos podem ser categorizados nos seguintes paradigmas de especificação:

  • Especificação baseada em histórico [3]
    • comportamento baseado em históricos do sistema
    • afirmações são interpretadas ao longo do tempo
  • Especificação baseada em estado [3]
    • comportamento baseado em estados do sistema
    • série de etapas sequenciais (por exemplo, uma transação financeira)
    • linguagens como Z , VDM ou B dependem deste paradigma [3]
  • Especificação baseada em transição [3]
    • comportamento baseado em transições de estado para estado do sistema
    • melhor usado com um sistema reativo
    • linguagens como Statecharts, PROMELA, STeP-SPL, RSML ou SCR contam com esse paradigma [3]
  • Especificação funcional [3]
    • especificar um sistema como uma estrutura de funções matemáticas
    • OBJ, ASL, PLUSS, LARCH, HOL ou PVS contam com este paradigma [3]
  • Especificação Operacional [3]
    • linguagens primitivas como Paisley , GIST, redes de Petri ou álgebras de processo contam com este paradigma [3]

Além dos paradigmas acima, existem formas de aplicar certas heurísticas para ajudar a melhorar a criação dessas especificações. O artigo referenciado aqui discute melhor a heurística a ser usada ao projetar uma especificação. [6] Eles fazem isso aplicando uma abordagem de dividir para conquistar .

Ferramentas de software

A notação Z é um exemplo de uma linguagem de especificação formal líder . Outros incluem a Linguagem de Especificação (VDM-SL) do Método de Desenvolvimento de Viena e a Notação de Máquina Abstrata (AMN) do Método B. Na área de serviços da Web , a especificação formal é frequentemente usada para descrever propriedades não funcionais [7] ( qualidade de serviço dos serviços da Web ).

Algumas ferramentas são: [4]

Exemplos

Para exemplos de implementação, consulte os links na seção de ferramentas de software .

Veja também

Referências

  1. ^ a b Hierons, RM; Bogdanov, K.; Bowen, JP ; Cleveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M .; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, AJH; Vilkomir, SA ; Woodward, MR; Zedan, H. (2009). "Usando especificações formais para suportar testes". Pesquisas de Computação ACM . 41 (2): 1. CiteSeerX  10.1.1.144.3320 . doi : 10.1145/1459352.1459354 . S2CID  10686134 .
  2. ^ a b c d e Gaudel, M.-C. (1994). "Técnicas de especificação formal". Anais da 16ª Conferência Internacional de Engenharia de Software . pp. 223-227. doi : 10.1109/ICSE.1994.296781 . ISBN 978-0-8186-5855-6. S2CID  60740848 .
  3. ^ a b c d e f g h i j k l m n o Lamsweerde, AV (2000). "Especificação formal". Anais da conferência sobre o futuro da engenharia de software - ICSE '00 . págs. 147-159. doi : 10.1145/336512.336546 . ISBN 978-1581132533. S2CID  4657483 .
  4. ^ a b c d Sommerville, Ian (2009). "Especificação formal" (PDF) . Engenharia de Software . Recuperado em 3 de fevereiro de 2013 .
  5. ^ a b c Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 de agosto de 2011). "Apoiando o desenvolvimento ágil, facilitando a interação natural do usuário com especificações formais executáveis". ACM SIGSOFT Notas de Engenharia de Software . 36 (4): 1–10. doi : 10.1145/1988997.2003643 . S2CID 2139235 . 
  6. ^ a b van der Poll, John A.; Paula Kotze (2002). "Que heurística de projeto pode aumentar a utilidade de uma especificação formal?" . Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology . SAICSIT '02: 179–194. ISBN 9781581135961.
  7. ^ Modelo de Conhecimento S-Cube: Especificação Formal

Links externos