首页 | 本学科首页   官方微博 | 高级检索  
     


Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applications
Authors:Doaa Soliman  Kleanthis Thramboulidis  Georg Frey
Affiliation:1. Chair of Automation, Saarland University, 66123 Saarbrücken, Germany;2. Electrical and Computer Engineering, University of Patras, Greece;1. Infectious Diseases, Department of Internal Medicine, Baylor College of Medicine, One Baylor Plaza, Mail Stop BCM286, Houston, TX 77030, USA;2. Department of Bioengineering, Rice University, Houston, Texas, USA;3. Department of Pathology, Baylor College of Medicine, Houston, Texas, USA;4. Department of Pathology, Stanford University School of Medicine, Stanford, California, USA;5. Cepheid, Sunnyvale, California, USA;6. Molecular Tuberculosis Laboratory, Houston Methodist Research Institute, Houston, Texas, USA;7. The Global TB Program, Texas Children''s Hospital, Houston, Texas, USA;8. Retrovirology and Global Health, Department of Pediatrics, Baylor College of Medicine, Houston, Texas, USA;9. Pulmonology, Department of Internal Medicine, Baylor College of Medicine, Houston, Texas, USA;1. Department of Electrical Engineering, Technion–Israel Institute of Technology, Haifa 3200003, Israel;2. Tower Semiconductor, Migdal Haemek 2310502, Israel;3. vSync Circuits, Yokneam Illit 2069201, Israel;4. Intel, Haifa 31015, Israel;5. Toga Networks, Hod Hasharon 4524075, Israel;1. The School of Computing, Korea Advanced Institute of Science and Technology (KAIST), Daejeon, Republic of Korea;2. The Chongqing Liangjiang KAIST International Program, Chongqing University of Technology (CQUT), Chongqing, China;1. National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai, China;2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China;3. Hardware/software Co-Design Technology and Application Engineering Research Center, East China Normal University, Shanghai, China
Abstract:Verification of IEC 61131-3 based safety applications is a challenge in the industrial automation domain. In this paper, the transformation of FBD diagrams to UPPAAL formal models was adopted to address this challenge. A set of transformation rules are defined for the automatic transformation of IEC 61131-3 Function Block based safety applications to UPPAAL timed automata models. These models are next used for the verification of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the definition of the transformation rules. Based on this a prototype model transformer was developed using Java. The transformer was used with various safety applications to check the efficiency of the transformation process. A laboratory system is presented as a case study to highlight the proposed approach.
Keywords:
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号