Abordagem sistemática para o controlo seguro de sistemas aeroespaciais

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. Estes estudos preliminares são efectuados no contexto de colaboração entre Investigadores dos centros de investigação CT2M, ALGORITMI e CCTC da Universidade do Minho (Portugal) e do Departamento de Engenharia Mecânica do Instituto Tecnológico de Aeronáutica (Brasil).

Formal verification of real-time systems behavior of is a complex task, for several reasons. There are multiple works developed in the domain of formal verification of real-time system behavior by model-checking, and various software tools were developed for this purpose. One of the most complexes problems to be solved in the analysis of real-time controllers is the conversion of programming languages controllers in formal languages, for example finite timed automata to be used as inputs of the existing model-checkers. If the methodology of the programming is well developed and known, this task can be greatly facilitated. Moreover, most real-time systems (especially embedded systems that we intend to study) are programmed in C language This article seeks to establish the methodology of creating programs in C code, from SFC specification formalism, taking into account the formal verification of behavior al properties desired for the system, using the Model-Checking technique and the modelchecker UPPAAL. A case study is presented to illustrate the methodology presented. These preliminary studies are presented on the context of a research collaboration project being developed by researchers of CT2M, ALGORITMI and CCTC research centers of University of Minho (Portugal) and the Mechanical Engineering Department of Technological Institute of Aeronautics (Brazil).