Elementos para a construção de uma cadeia de verificação para o projeto TopCased

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-graduação em Automação e SistemasAnalisando a história dos sistemas embarcados, podemos dividi-la em dois momentos. Em um primeiro momento, a origem dos problemas destes sistemas provinha, na grande maioria dos casos, da parte física chamada hardware. A partir dos anos 60, graças à chegada dos circuitos integrados, desenvolvidos para o Programa Espacial Americano, a parte física dos sistemas se tornou mais confiável. Nós últimos 20 anos, devido à complexidade inerente ao desenvolvimento dos softwares para sistemas embarcados, estes se tornaram a origem da maior parte dos erros. Uma das grandes dificuldades no desenvolvimento destes softwares é assegurar um funcionamento correto (de acordo com as especificações). A fim de reduzir a incidência de erros, a indústria passou a estudar o uso de métodos formais para auxiliar o desenvolvimento destes sistemas complexos. Estas técnicas auxiliam o processo decisório porque permitem afirmar antes de implementar o protótipo se uma dada especificação será cumprida ou não pelo sistema. Entretanto, a verificação formal ainda não é largamente empregada no ambiente industrial devido à dificuldade no intercâmbio de informações entre as linguagens de modelagem de alto nível (UML, AADL, SDL, etc) e as ferramentas de verificação formal. Esta dificuldade é decorrente da falta de uma semântica formal para estas linguagens de modelagem largamente utilizadas pela indústria. Além disto, cada ferramenta de verificação trabalha com formalismos matemáticos diferentes, não havendo uma fácil integração entre elas. Outro fator importante é que não podemos afirmar que existe um formalismo único capaz de atender a todas as necessidades de um sistema complexo. Isto implica que sistemas futuros vão cada vez mais requerer uma combinação de métodos baseados em modelos, tais como sistema de transição, álgebra de processos, lógica temporal, entre outros. Estas restrições impõem à indústria a necessidade de desenvolver uma ferramenta de tradução de modelos para cada par linguagem-formalismo empregado. A fim de facilitar este intercâmbio de informações entre as diferentes linguagens de modelagem e as ferramentas de verificação formais existentes - tais como TINA (Time Petri Net Analyser), CADP (Construction and Analysis of Distributed Processes), entre outras - o projeto TOPCASED (Toolkit in Open-Source for Critical Application & Systems Development) desenvolveu uma arquitetura de verificação original, que promove a transformação de modelos entre os diferentes níveis. Esta transformação é simplificada pelo advento de uma linguagem intermediária formal chamada FIACRE (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués). Dentro deste contexto, as atividades desenvolvidas neste trabalho fazem parte da especificação e operacionalização da linguagem FIACRE do projeto TOPCASED. A primeira atividade apresentada neste trabalho é o estudo preliminar da tradução entre SDL e FIACRE para auxiliar na especificação da linguagem FIACRE. A segunda atividade consiste inicialmente na proposição de um esquema conceitual para a tradução de FIACRE para o formalismo matemático TTS (Sistema de Transições Temporizadas), e posteriormente na sua implementação na forma de um compilador (front-end) para a ferramenta TINA. Por último, um exemplo de verificação de sistema é apresentado com o intuito de demonstrar as vantagens das ferramentas que fazem parte do projeto TOPCASED