A verificação formal do comportamento de sistemas tempo-real é uma tarefa complexa, por várias razões. Há múltiplos trabalhos desenvolvidos na área de verificação formal, por model-checking de sistemas tempo-real, sendo que diversos softwares foram desenvolvidos para o efeito. Um dos problemas mais complexos para serem resolvidos na análise de controladores tempo-real é a conversão das linguagens de programação dos controladores nas linguagens formais, por exemplo autómatos finitos temporizados para depois poderem ser verificados formalmente através dos model-checkers existentes. Se a metodologia de elaboração dos programas for bem desenvolvida e conhecida, essa tarefa pode ser muito facilitada. Por outro lado, grande parte dos sistemas tempo-real (principalmente os sistemas embebidos que pretendemos estudar) é programado em linguagem C. Neste artigo pretende-se estabelecer uma metodologia de criação de programas em código C, a partir do formalismo de especificação SFC, tendo em conta a verificação formal de propriedades comportamentais desejadas para o sistema, utilizando a técnica Model-Checking e o model-checker UPPAAL.

@InProceedings{BorgesVMFC:2010b,
 author = {P. Borges and E. Villani and J. Machado and J. Ferreira and J. Campos},
 title = {Abordagem Sistemática para o Controlo Seguro de Sistemas aeroespaciais},
 booktitle = {XIV International Congress on Project Engineering},
 year = {2010},
 pages = {2666-2676},
 publisher = {FGUPM},
 abstract = {A verificação formal do comportamento de sistemas tempo-real é uma tarefa complexa, por várias razões. Há múltiplos trabalhos desenvolvidos na área de verificação formal, por model-checking de sistemas tempo-real, sendo que diversos softwares foram desenvolvidos para o efeito. Um dos problemas mais complexos para serem resolvidos na análise de controladores tempo-real é a conversão das linguagens de programação dos controladores nas linguagens formais, por exemplo autómatos finitos temporizados para depois poderem ser verificados formalmente através dos model-checkers existentes. Se a metodologia de elaboração dos programas for bem desenvolvida e conhecida, essa tarefa pode ser muito facilitada. Por outro lado, grande parte dos sistemas tempo-real (principalmente os sistemas embebidos que pretendemos estudar) é programado em linguagem C. Neste artigo pretende-se estabelecer uma metodologia de criação de programas em código C, a partir do formalismo de especificação SFC, tendo em conta a verificação formal de propriedades comportamentais desejadas para o sistema, utilizando a técnica Model-Checking e o model-checker UPPAAL.}
}

Generated by mkBiblio 2.6.28