Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/18103
Título: | A formal approach for safe controllers analysis |
Autor(es): | Borges, Paulo Machado, José Mendes Seabra, Eurico Lima, Mário |
Palavras-chave: | Safe controllers Real-time systems Embedded systems Formal verification Specification formalisms |
Data: | 2010 |
Editora: | Cefin Publishing House |
Revista: | Romanian Review Precision Mechanics, Optics and Mecatronics |
Resumo(s): | Formal verification of real-time systems software is a complex and hard task, for several reasons. There are multiple works developed in the domain of formal verification of real-time systems behavior by model-checking, and some software tools were developed for this purpose. One of the most complex problems to be solved in the analysis of real-time controllers is the conversion of controllers programming languages in formal languages, for instance finite timed automata, in order to be used as inputs of the existing model-checkers. If the methodology of programming is well developed and known, this task can be improved in order to improve safety and reliability of the obtained controllers. Moreover, most real-time systems (especially embedded systems that we intend to study) are programmed in C language. This paper aims to establish the methodology of creating C code programs, from SFC specification formalism, taking into account the formal verification of desired properties for the system behavior, using the Model-Checking technique and the model-checker UPPAAL. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/18103 |
ISSN: | 1584-5982 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | DEM - Artigos em revistas de circulação internacional com arbitragem científica |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Paper_1 FINAL JMachado_Portugal.pdf | 312,17 kB | Adobe PDF | Ver/Abrir |