A cada dia que se passa, o ser humano vai se tornando mais dependente de soluções tecnológicas, tanto para enfrentar problemas presentes quanto para enfrentar desafios futuros. Uma das soluções tecnológicas que mais vem crescendo para auxiliar o ser humano são as soluções computacionais. Dentre essas soluções computacionais podemos destacar as baseadas em software. Cada vez mais, desafios com problemas mais complexos tem forçado a criação de soluções computacionais complexas, principalmente em problemas onde falhas não podem ser toleradas e mesmo que estas ocorram existam soluções que neutralizem estas falhas. Todavia, elaborar soluções computacionais complexas não é trivial onde, por natureza, tendem a surgir falhas durante a elaboração do projeto. É sabido que elaborar sistemas computacionais isentos totalmente de falhas não é possível, contudo é possível elaborar sistemas computacionais com menor taxa de erros possível, principalmente quando estes sistemas são complexos e visam atender problemas complexos, onde diversos riscos podem acontecer como: riscos ao meio ambiente, riscos à vida do ser humano e demais seres vivos, riscos monetários, riscos à segurança e etc..
Elaborar sistemas complexos através de linguagem descritiva, como a Língua Portuguesa, pode acarretar problemas de ambiguidade na expressão de ideias. Então métodos semiformais, como a UML, surgem para resolver este problema. Porém, com o uso da UML não é possível obter uma consistência e grau de completude de alto nível e de grande precisão, principalmente devido as novas tecnologias não conseguirem ser modeladas coerentemente nesta notação. É aí onde entram os Métodos Formais para resolução destes problemas.
Métodos Formais são métodos utilizados para elaboração de sistemas computacionais dando prioridade a sua coesão, isto porque estes métodos são desenvolvidos a partir de princípios matemáticos que garantem a sua exatidão na capacidade de expressão das ideias vinculadas ao projeto de software. Estes métodos foram desenvolvidos para auxiliar todas as etapas de desenvolvimento de software, sendo elas: especificação formal para definição de requisitos, refinamento para concepção de projeto, síntese para implementação, prototipagem para a validação e prova para a verificação. Além disso, o uso de Métodos Formais poder ser aplicado durante todas as etapas de desenvolvimento do software ou somente em algumas etapas ou partes do projeto de desenvolvimento. Os Métodos Formais também podem ser utilizados para modelar desenvolvimento de sistemas de hardware.
A seguir serão explicitados sucintamente cada uma das etapas em que se aplica os métodos formais e, por último, algumas notações formais mais utilizadas no meio acadêmico e das indústrias de TI.
Especificação Formal
Semelhante ao processo de identificação de Requisitos, nesta etapa são identificados os Requisitos Funcionais e os Requisitos Não Funcionais do sistema. Requisitos Funcionais correspondentes ao que o software deve fazer e os Requisitos Não Funcionais correspondentes a como o software deverá executar seus procedimentos e rotinas para desempenhar o que foi designado para o seu fim.
Os maiores problemas que acontecem na fase de Elicitação de Requisitos é referente a incompletude ou os requisitos não expressarem claramente a realidade do que o cliente realmente deseja do sistema. Principalmente, sistemas onde a maior quantidade de requisitos possíveis precisa ser descoberta e que estejam bem definidos para que o processo de software prossiga para a próxima etapa. Devido a isto, uma alternativa é o uso de Especificação Formal.
Especificação Formal consiste em formalizar os requisitos descobertos utilizando algum método formal, criando uma modelagem com o uso de elementos. Estes elementos podem variar de acordo com o método formal utilizado, por exemplo: uso de Teoria de Conjuntos em notação B ou Z, uso de Álgebra de Processos em notação LOTOS e etc.. É de extrema importância que esta fase seja acompanhada de uma descrição textual dos requisitos, para que estes possam ser facilmente revisados com o cliente facilitando a interação com o mesmo. A Especificação Formal trata-se de uma fase dentro da etapa de Requisitos para analisar a consistência das informações.
Nesta fase não basta somente modelar os requisitos, é necessário analisar também circunstâncias que levam ao relacionamento entre requisitos como:
- Interfaces com o ambiente;
- Noção de estados do sistema;
- Noção de comportamentos;
- Noção de requisitos de segurança;
- Nível de integridade do software.
Refinamento
A fase de refinamento é utilizada para conceber o projeto de software, ou seja, nesta fase é pensado na arquitetura do sistema com seus diversos componentes e suas interfaces, dados e relacionamentos entre os mesmos. Esta fase consiste na criação e manutenção de um modelo do sistema, analisando o seu comportamento estático e dinâmico, expressando os procedimentos para cumprir com as finalidades especificadas para o sistema. São pensadas nas atividades e suas sequências de execução, funções para cumprir as atividades, entradas e saídas do sistema.
Algumas ferramentas para utilização de métodos formais possuem interface gráfica, facilitando o refinamento por meio de utilização de componentes gráficos. O uso de componentes gráficos permite simular atividades do sistema para avaliar o seu comportamento.
Síntese
A fase de Síntese consiste em, a partir do modelo refinado, gerar esqueleto de código, que pode servir como base para implementação real do sistema. Algumas ferramentas já fornecem auxílio nesta fase, muitas delas geram código na linguagem C ou Java.
Prototipagem e Prova
A fase de Prova é utilizada para verificar se o sistema desenvolvido foi concebido atendendo a todos os Requisitos Funcionais e Não-Funcionais elicitados. A fase de Prototipagem consiste em elaborar um protótipo funcional do sistema para validar se o mesmo, atende as necessidades do cliente.
A fase de prova pode ser realizada de duas maneiras: prova de teorema automatizada e verificação de modelo. A prova de teorema automatizada consiste em utilizar uma descrição do sistema, aplicando inferências lógicas verificando o grau de correção do sistema; pode ser feita em todo o sistema ou somente em partes que o profissional ache mais vulneráveis. A prova de verificação de modelo é realizada fazendo uso do modelo construído na fase de Refinamento; neste procedimento é realizado fazendo testes exaustivos em todos os estados em que o sistema poderá se comportar; geralmente estes testes são feitos para verificar propriedades não funcionais por exemplo.
A partir da fase de prova, é possível proceder para a fase de Prototipagem fazendo testes em protótipos, onde será possível validar as necessidades do cliente com relação ao sistema. Assim, o uso do esqueleto de código gerado pelas ferramentas formais na fase de síntese, pode ser uma ótima alternativa.
Exemplos de Linguagens Formais
Assim como a notação UML é utilizada para modelagem semiformal no processo de software, os Métodos Formais também dispõem de notações das mais variadas. Conhecidas como linguagens ou notações formais, estes podem ser baseados em diversos segmentos matemáticos, dos mais simples aos mais complexos. O fato de os Métodos Formais serem baseado em Matemática, constituem uma barreira para que sejam implantados como recursos, utilizados pelos profissionais, nas empresas devido a necessidade que se faz aprender e ter domínio dos mesmos. Outro fator, é que o uso de Métodos Formais torna o processo de software oneroso. A seguir será descrito, sucintamente, algumas notações.
Notação Z
A notação Z foi criada na Universidade de Oxford, na década de 70. Esta notação é baseada em teoria de conjuntos, para especificar as informações e operações do sistema e lógica de predicado de primeira ordem, para representar seus comportamentos e propriedades. Todo o processo de especificação é baseado no uso de esquemas. Os esquemas são estruturas lógicas compostas por duas partes, declarativa e predicativa; ambos fazendo uso de Teoria de Conjuntos. Na parte declarativa são feitas as declarações de variáveis baseadas em elementos da Teoria de Conjuntos. Na parte predicativa é feita a relação entre estas variáveis, inclusive com esquemas e variáveis de outros esquemas já posteriormente declarados. Veja um modelo na Figura 1.
Figura 1. Modelo de um esquema
Existem algumas ferramentas com suporte a esta notação. A ZWordTools é uma ferramenta para especificação na notação Z, que consiste em um plugin para o programa Word da Microsoft, com ela é possível especificar, checar, gera modelos gráficos e etc.. Esta ferramenta pode ser obtida na sua página principal. Um modelo da sua interface pode ser visto na Figura 2.
A ferramenta CZT é baseada na IDE do eclipse permitindo que sejam criados projetos baseados na notação Z, esta ferramenta também pode ser facilmente incorporada a própria IDE Eclipse e pode ser encontrada no seu site oficial.Podemos conferir como é a sua interface gráfica na Figura 3.
Figura 2. Interface Gráfica da ferramenta ZWordTools
Figura 3. Interface Gráfica da ferramenta CZT
Notação B
A notação B foi desenvolvida pela Oxford na década de 80, baseada em Teoria dos Conjuntos e Lógica de Predicados também. Foi projetada para as fases de especificação, refinamento e síntese. A fase de especificação faz uso de máquinas de estados compostas de: Estado, Invariante e Operações.
O Estado corresponde a declaração de variáveis e estados do sistema. A invariante corresponde aos predicados lógicos aplicados sobre as variáveis e determinação dos estados válidos do sistema. As Operações modificam ou consultam os estados do sistema.
Dentre as ferramentas que podem ser utilizadas são, podemos destacar a AtelierB, B4freee ProB.
Na Figura 4 você confere a interface gráfica da ferramenta AtelierB.
Figura 4. Interface Gráfica da ferramenta AtelierB e modelo de especificação do método B.
Outras linguagens formais
Outros tipos de linguagens formais que foram desenvolvidas são a CSP (Communicating Sequential Processes) que foi desenvolvida para especificação de Sistemas Concorrentes; esta notação é baseada em Álgebra de Processos, ou seja, faz uso de Álgebra para especificação de processos relacionados a comportamentos e atividades em sistemas concorrentes; uma ferramenta para especificação em CSP é a PAT. Outra linguagem que também é baseada em Álgebra de Processos é LOTOS (Language Of Temporal Ordering Specification) e ferramentas podem ser encontradas no site LOTOS Utilities. A notação Redes de Petri é baseada em várias representações matemáticas fazendo uso de grafos para especificação de Sistemas Distribuídos discretos. Dentre as ferramentas disponíveis no mercado, podemos destacar a WoPED.
Como pode ter sido observado neste artigo, foi realizada uma breve introdução aos Métodos Formais, etapas onde podem ser empregados, vantagens e desvantagens, além de algumas notações e ferramentas de suporte. Espero que tenham gostado deste artigo. Obrigado pela atenção de vocês e até a próxima.
