Sistemas híbridos: modelagem, verificação e ferramentas Arnaldo Moura — IC/UNICAMP

\underline{Cenário}: É cada vez mais comum a presença de sistemas híbridos, resultantes da integração entre ambientes analógicos e controladores discretos. Frequentemente, tais sistemas são formados por vários módulos distribuídos que devem cooperar para atingir objetivos comuns. Em resposta a esta evolução, surge a necessidade de modelar tais sistemas de modo a permitir a análise e a verificação rigorosas de propriedades do sistema completo. Destes modelos devem resultar ferramentas computacionais (semi-)automáticas que viabilizem a verificação de sistemas de porte razoável.

\underline{Modelos}: Autômatos híbridos surgiram como um modelo natural para sistemas híbridos. Um autômato híbrido é formado por um autômato finito (clássico) que descreve o controle discreto do sistema. Este autômato finito é equipado com um conjunto de variáveis contínuas, que evoluem segundo leis dinâmicas, e que descrevem a parte analógica do sistema. Cada módulo do sistema é descrito por um autômato híbrido. O sistema distribuído completo é descrito pelo produto destes autômatos, garantindo mecanismos de sincronização entre os componentes. Cada componente já introduz um número infinito de estados no modelo, através das variáveis contínuas. O produto gera, ainda, uma explosão combinatória no número de componentes discretas nos estados do autômato resultante.

\underline{Palestra}: Nesta palestra, vamos explorar o potencial da modelagem de sistemas integrados através de autômatos híbridos. A noção de autômato híbrido será apresentada. Exemplos típicos serão discutidos. Em seguida, as propriedades do modelo serão exploradas, mostrando quais restrições a parte contínua deve satisfazer para garantir a (semi-)decidabilidade das propriedades básicas necessárias para a verificação do modelo. Nos casos indecidíveis, serão examinadas abordagens aproximativas como alternativas às soluções exatas. Serão mencionadas algumas ferramentas, já implementadas, que realizam verificação (semi-)automática de sistemas híbridos. O grau de sucesso destas ferramentas pode ser aquilatado através dos exemplos práticos onde foram usadas.