Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/18103

TitleA formal approach for safe controllers analysis
Author(s)Borges, Paulo
Machado, José Mendes
Seabra, Eurico
Lima, Mário
KeywordsSafe controllers
Real-time systems
Embedded systems
Formal verification
Specification formalisms
Issue date2010
PublisherCefin Publishing House
JournalRomanian Review Precision Mechanics, Optics and Mecatronics
Abstract(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.
TypeConference paper
URIhttps://hdl.handle.net/1822/18103
ISSN1584-5982
Peer-Reviewedyes
AccessOpen access
Appears in Collections:DEM - Artigos em revistas de circulação internacional com arbitragem científica

Files in This Item:
File Description SizeFormat 
Paper_1 FINAL JMachado_Portugal.pdf312,17 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID