O Papel da Especificação Formal no Desenvolvimento de Sistemas de Software

 

O rápido avanço da tecnologia requer, cada vez mais, formas mais rápidas e confiáveis de desenvolver sistemas de software a fim de atender aos requisitos de usuários e sistema. É, portanto, essencial a esses desenvolvedores utilizar técnicas de especificação que ofereçam suporte, ao que costumo denominar de 5 C’s, isto é: corretude, completude, consistência, concisão e clareza. Concomitante a isto, é ainda de suma importância que a técnica de especificação possua um conjunto de conceitos bem definidos e base matemática de modo a permitir a construção e uso de ferramentas computacionais para analisar e simular especificações, bem como verificar a conformidade de implementações com as respectivas especificações.

Neste sentido, uma técnica de especificação formal, fazendo uso de conceitos bem definidos e modelo matemático, é usada para representar propriedades significativas de um sistema. O uso de formalismo durante a especificação permite a eliminação de ambigüidades, inconsistências às quais apenas seriam detectadas mais tarde durante fases de implementação e testes do ciclo de desenvolvimento de um sistema. A correção da especificação num estágio preliminar do desenvolvimento evita que erros sejam corrigidos tardiamente e, portanto, resultem em ser mais onerosos. Agora, o leitor pode questionar: Em que situações a especificação formal poderia ser utilizada?

Neste contexto, um dos principais desafios com o qual desenvolvedores de software se deparam é o de assegurar a confiabilidade de sistemas projetados. Esse objetivo torna-se ainda mais imperativo quando software é empregado em sistemas cuja falha operacional podem ocasionar perdas humanas, econômicas ou causar degradação na prestação de serviços. Em ambientes críticos envolvendo sistemas de controle de tráfego aéreo ou de comando e controle de aeronaves, há uma necessidade preeminente de que os requisitos do sistema sejam precisamente especificados, objetivando implementar corretamente o projeto. Situação similar ocorre em sistemas sujeitos a sofrer degradação no nível de prestação de serviços quando operando em situação de falha. Exemplos de tais sistemas compreendem os sistemas de telecomunicações e sistemas de bancos com caixa de auto-atendimento. Tais sistemas enquadram-se dentro da categoria de sistemas reativos e compreende os sistemas para os quais as técnicas de especificação formal apresentadas podem ser empregadas.

Cabe ainda salientar que, em geral, uma especificação engloba diversos aspectos de sistema como, por exemplo, requisitos comportamentais, não comportamentais, consumo de energia, dimensões física, dentre outros. Dentro desse conjunto, os requisitos comportamentais de sistemas são de suma importância para a classe de sistemas reativos e várias técnicas de especificação formal, como Statecharts e SDL (Specification and Description Language) podem ser empregadas na especificação desses sistemas. A especificação de um sistema compreende várias informações, devendo cada uma delas ser expressa numa linguagem ou técnica apropriada. Embora a linguagem natural constitua uma alternativa para descrever objetivos, metas e requisitos, ela não consegue capturar precisamente e sem ambigüidades os requisitos de um sistema. Consequentemente, técnicas de especificação formal têm sido empregadas para especificar sistemas complexos.

Adicionalmente, para que engenharia de software possa ser considerada uma disciplina de engenharia de fato, torna-se necessário a adoção de técnicas de especificação formal a fim de empreender mais rigor e precisão na especificação de sistemas, objetivando minimizar ao máximo ou, quiçá, eliminar totalmente erros existentes. Satisfazer este objetivo é imperativo em sistemas como, por exemplo, controle de tráfego aéreo, telecomunicações e caixas de auto atendimento de bancos. Note que se algum desses sistemas falhar ou deixar de operar, isto pode implicar em degradação da qualidade de serviços oferecidos, prejuízos financeiros e até perdas humanas (no caso de sistemas críticos). Portanto, assegurar a corretude de funcionamento de um sistema, significa garantir disponibilidade de serviços e confiabilidade operacional.

Concluindo, as técnicas de especificação formal estão cada vez mais se consolidando como ferramenta essencial para a produção de software. Utilizando a base matemática de uma técnica de especificação formal, torna-se possível explorar o projeto de modo mais preciso e rigoroso bem como permite verificar propriedades das especificações e projeto, e ainda analisar de maneira sistemática o comportamento do sistema de software antes de produzi-lo.

Informações complementares e links relevantes é apresentado ao leitor no site http://www.comlab.ox.ac.uk/archive/formal-methods.html