Title: Model Checking application on Function Block Diagram model
Authors: Ausberger, Tomáš
Kubíček, Karel
Medvecová, Pavla
Myslivec, Tomáš
Štětina, Milan
Citation: AUSBERGER, T., KUBÍČEK, K., MEDVECOVÁ, P., MYSLIVEC, T., ŠTĚTINA, M. Model Checking application on Function Block Diagram model. In: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. New York: IEEE, 2020. s. 1807-1814. ISBN 978-1-72818-956-7, ISSN 1946-0740.
Issue Date: 2020
Publisher: IEEE
Document type: konferenční příspěvek
URI: 2-s2.0-85093357615
ISBN: 978-1-72818-956-7
ISSN: 1946-0740
Keywords in different language: Formal model;Functional Block Diagram;Model Checking;model conversion;nuclear power plant;REXYGEN;safety-critical system;SMV;verification
Abstract in different language: Model Checking represents a mathematical method of formal verification which can prove that model satisfies its specified requirements. This article describes an approach that utilizes Function Block Diagram (FBD) models. The key benefit of this approach is the automatic transformation of the original model into a formal model which can be checked by Model Checking. In this way Model Checking can be easier integrated in the standard development process. The presented approach was developed together with the new verification process. This process can be used for the verification of safety-critical systems.
Rights: Plný text není přístupný.
Appears in Collections:Konferenční příspěvky / Conference papers (NTIS)
Konferenční příspěvky / Conference Papers (KKY)

Files in This Item:
File SizeFormat 
09212180.pdf515,23 kBAdobe PDFView/Open    Request a copy

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

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

  1. DSpace at University of West Bohemia
  2. Publikační činnost / Publications
  3. OBD