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

TitleA specification patterns system for discrete event systems analysis
Author(s)Campos, J. Creissac
Machado, José Mendes
KeywordsDiscrete event systems
Dependability
Model checking
Property specification patterns
Issue date2013
PublisherInTech
JournalInternational Journal of Advanced Robotic Systems
Abstract(s)As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express properties of a system's behavior is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skillful process. Errors in this step of the process can create serious problems since a false sense of safety is gained with the analysis. However, when compared to the effort put into developing and applying modeling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements.
TypeArticle
URIhttp://hdl.handle.net/1822/26489
DOI10.5772/56412
ISSN1729-8806
Publisher versionhttp://www.intechopen.com/journals/international_journal_of_advanced_robotic_systems/a-specification-patterns-system-for-discrete-event-systems-analysis
Peer-Reviewedyes
AccessOpen access
Appears in Collections:HASLab - Artigos em revistas internacionais

Files in This Item:
File Description SizeFormat 
CamposM2013-A_specification_patterns_system_for_discrete_event_systems_analysis.pdfeditor's version1,98 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