A Vós a Razão
Assegurar a qualidade e confiabilidade de sistemas computacionais
Por Alexandre Madeira*
É Natal, época de alegria, partilha e convívio. Há as crianças, a família, os amigos, croquetes e rabanadas, e também as perguntas tipo “o que é que andas a fazer?”, seguidas das inevitáveis “mas afinal para que é que isso serve?”. Este ano houve ainda o desafio da “A Vós a Razão” para que escrevesse qualquer coisa interessante sobre o meu trabalho no HASLab INESC TEC. É com muito prazer e boa vontade, mas com o espírito de superação que sentimos, nas madrugadas de 1 de janeiro, ao prometer substituir religiosamente todo o fast-food por uma ementa rica em antioxidantes ou organizar aquela pasta matrioska que há anos nos decora o desktop recheada de PDFs interessantes por desbravar, que espremerei a minha veia cronista nesta folha A4 (regulamentar). Uso as perguntas acima como muleta.
Se até as mentes mais pragmáticas se compadecem com as virtudes da aplicabilidade imediata de lógicas formais no desenvolvimento e validação de sistemas computacionais complexos, já o interesse prático do desenvolvimento de métodos genéricos para a construção destes formalismos, juntamente com caracterizações de propriedades abstratas sobre os formalismos obtidos, tem levantado o ceticismo da parte de alguns entusiastas das ciências mais puras. Aproveito esta oportunidade para desmistificar um pouco este aparente fosso, dando-vos conta do que andamos a fazer, como o aplicamos e, principalmente, o potencial aplicativo que convictamente identificamos nestes trabalhos.
Assegurar a qualidade e confiabilidade de sistemas computacionais pela aplicação de técnicas da matemática e da lógica formal é o objetivo que tem movido a equipa com quem tenho tido o privilégio de aprender e trabalhar. Estas técnicas, denominadas de Métodos Formais, têm despertado um progressivo interesse na indústria, não só pelos inúmeros casos-de-estudo de sucesso (e.g. na Rockwell Collins, Intel, etc.), como pela sua recomendação em standards (e.g. no EN 50126/8/9 – Railway Application: Demonstration of Reliability and Safety e no DO178C – Software Considerations in Airborne Systems and Equipment Certification) ou, em alguns casos, mesmo a mandotariedade de algum nível da sua aplicação (ISO/IEC 1540 – Common Criteria for Information Technology Security Evaluation).
Os projetos em que estou envolvido centram-se na definição de lógicas adequadas ao tratamento de sistemas computacionais. No essencial, este esforços têm-se traduzido na definição de fundamentos e métodos para a construção de lógicas dedicadas a problemas específicos. A novidade da abordagem é a perspetiva "on-demand" que adotámos: olha-se para o sistema em mãos, reconhecem-se os “ingredientes” lógicos necessários para o tratar, e aplicam-se os nossos métodos para a construção de uma novas lógicas adequadas ao design e validação dos sistemas pretendidos. Foi esta a motivação de base para a definição do método de “hibridização de lógicas” introduzido no meu doutoramento e com o qual construímos uma gama de novas lógicas adequadas ao tratamento de uma grande variedade de sistemas reconfiguráveis (desde estruturas elásticas de armazenamento em "cloud" a sistemas computacionais com estrutura hierárquica nos estados).
O nosso recente projeto em “dinamização de lógicas”, outro método para a construção “on-demand” de lógicas para uma vasta gama de sistemas reativos, segue uma estrutura similar. Apesar de estar ainda a traçar os seus primeiros passos, já foi com ele que introduzimos algumas lógicas para a verificação de sistemas muito desafiantes, nomeadamente, de sistemas cujos comportamentos dependem da gestão de recursos (e.g. energia em robots submarinos), de sistemas íntegros para agir em cenários de incerteza (e.g. confiança de sensores), ou de agentes que reagem probabilisticamente em contexto de missão. Todos os exemplos estendem, a estes novos paradigmas computacionais, a técnica clássica da verificação de programas imperativos pelo uso dos famosos triplos de Hoare. É ainda nossa intenção explorar este método enquanto fonte de lógicas adequadas à validação formal de controladores industriais desenvolvidos sob o standard IEC 61131-3, um projeto que está a dar os primeiros passos em colaboração com o CROB.
Em jeito de última nota, gostaria de enfatizar que a versatilidade e aplicabilidade destes métodos têm sido alcançadas como corolário de um forte investimento na sua componente fundamental de matemática. No contexto difícil em que hoje vivemos, onde a apologia da aplicabilidade óbvia e imediata se respira no ar, é de enaltecer a visão estratégica desta casa ao perceber que o motor para a inovação, sustentável e inesgotável, terá sempre que se suportar num trabalho de backstage em desenvolvimentos teóricos e tarefas experimentais. Verdade à La Palisse, dirão... Um abraço de feliz ano novo!
* Colaborador no Laboratório de Software Confiável (HASLab)
