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

TitleUsing timed automata for modeling, simulating and verifying networked systems controller's specifications
Author(s)Kunz, Guilherme
Machado, José
Perondi, Eduardo
KeywordsIEC 61850 communication requirements
Simulation
Formal verification
Timed automata
Automated people movers
Issue date2017
PublisherSpringer
JournalNeural Computing & Applications
Abstract(s)The development of dependable controllers can be a very complex task. For this purpose, some synthesis and analysis modern computational techniques can be used. In this paper, simulation and formal verification analysis techniques are used in a concurrent way in order to validate formal communication requirements of generic object oriented substation event and sample value communication protocols from the IEC 61850 standard. Because these techniques are used in a complementary way, the formalism and tools used for both are the same: timed automata for modeling, and UPPAAL model checker for performing simulation and formal verification tasks. Also, we show that the use of timed automata formalism is suitable for modeling the controllers' specifications, specifying the time requirements for information exchanging taking into account networked controllers, and, as it is a non-deterministic formalism, for analyzing the plant behavior. The concepts developed in this study were successfully tested in an application in the control system of an automated people mover.
TypeArticle
URIhttp://hdl.handle.net/1822/53617
DOI10.1007/s00521-015-2115-5
ISSN0941-0643
Peer-Reviewedyes
AccessRestricted access (UMinho)
Appears in Collections:CT2M - Artigos em revistas de circulação internacional com arbitragem científica

Files in This Item:
File Description SizeFormat 
RI_WoS_14.pdf
  Restricted access
1,39 MBAdobe 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