@conference {BorgesVMFC:2010b,
	title = {Abordagem Sistem{\'a}tica para o Controlo Seguro de Sistemas aeroespaciais},
	booktitle = {XIV International Congress on Project Engineering},
	year = {2010},
	month = {June},
	pages = {10p},
	address = {Madrid, Spain},
	abstract = {<p>A verifica{\c c}{\~a}o formal do comportamento de sistemas tempo-real {\'e} uma tarefa complexa, por v{\'a}rias raz{\~o}es. H{\'a} m{\'u}ltiplos trabalhos desenvolvidos na {\'a}rea de verifica{\c c}{\~a}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{\'a}lise de controladores tempo-real {\'e} a convers{\~a}o das linguagens de programa{\c c}{\~a}o dos controladores nas linguagens formais, por exemplo aut{\'o}matos finitos temporizados para depois poderem ser verificados formalmente atrav{\'e}s dos model-checkers existentes. Se a metodologia de elabora{\c c}{\~a}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) {\'e} programado em linguagem C. Neste artigo pretende-se estabelecer uma metodologia de cria{\c c}{\~a}o de programas em c{\'o}digo C, a partir do formalismo de especifica{\c c}{\~a}o SFC, tendo em conta a verifica{\c c}{\~a}o formal de propriedades comportamentais desejadas para o sistema, utilizando a t{\'e}cnica Model-Checking e o model-checker UPPAAL.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jccampos/files/ciip10_2666_2676.2958.pdf},
	author = {P. Borges and E. Villani and J. Machado and Jos{\'e} Creissac Campos and Jo{\~a}o F.}
}