Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/38816
Título: | Abordagem sistemática para o controlo seguro de sistemas aeroespaciais |
Autor(es): | Borges, Paulo André Mendes Machado, José Ferreira, João Amaro Oliveira Campos, J. Creissac Villani, Emilia |
Palavras-chave: | Controladores seguros Sistemas tempo-real Sistemas embebidos Verificação formal Formalismos de especificação do comando Safe controllers Real-time systems Embedded systems Formal verification Specification formalisms |
Data: | 2010 |
Resumo(s): | 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). |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/38816 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |