Safety Property Comparison Between Grobner Bases and BDD-based Model Checking Method

被引：0

作者：

Alwi, Saifulza ^{[1
]}

Fujimoto, Yasutaka ^{[2
]}

机构：

[1] Univ Teknikal Malaysia Melaka, Fac Elect Engn, Hang Tuah Jaya 76100, Melaka, Malaysia

[2] Yokohama Natl Univ, Fac Engn, Dept Elect & Comp Engn, Hodogaya Ku, 79-5 Tokowadai, Yokohama, Kanagawa 2408501, Japan

来源：

2014 13TH INTERNATIONAL CONFERENCE ON CONTROL AUTOMATION ROBOTICS & VISION (ICARCV) | 2014年

关键词：

FORMAL VERIFICATION; SYSTEMS;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Implementation of verification procedures is required to eliminate design errors that decrease the safety of an automation system. Design errors may vary from case to case but will certainly jeopardize the safety of manufacturing lines and operators. Therefore, checking the possibility of state transitions in the control systems from safe to unsafe states is essential. Formal verification via model checking procedures has proven to be efficient and is widely used. System finite element models are employed to automatically verify certain correctness properties. In this paper, we introduce a method of model checking technique for logic control design. A checking procedure based on Grobner bases (GB) model is used to analyze and design a controller that meets the requirements defined by a predetermined safety function. We compare our proposed method with symbolic computation tree logic (CTL) model checking based on binary decision diagrams (BDDs). We implemented this technique to a case study by using a crane system.

引用

页码：511 / 516

页数：6

共 50 条

[31] Probabilistic abstraction for model checking: An approach based on property testing
Laplante, Sophie
Lassaigne, Richard
Magniez, Frederic
Peyronnet, Sylvain
De Rougemont, Michel
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2007, 8 (04)
[32] System safety assessment based on STPA and model checking
Dakwat, Alheri Longji
Villani, Emilia
SAFETY SCIENCE, 2018, 109 : 130 - 143
[33] Hierarchical Model Checking Method of Safety Communication Protocol Specification
Zhang Y.
Yang L.
Zeng X.
Sun W.
Liu Q.
Zhongguo Tiedao Kexue/China Railway Science, 2021, 42 (06): : 162 - 170
[34] Effective safety property checking using simulation-based sequential ATPG
Sheng, S
Takayama, K
Hsiao, MS
39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002, 2002, : 813 - 818
[35] Property-Driven Design for Robot Swarms: A Design Method Based on Prescriptive Modeling and Model Checking
Brambilla, Manuele
Brutschy, Arne
Dorigo, Marco
Birattari, Mauro
ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2015, 9 (04)
[36] BDD vs. constraint-based model checking: An experimental evaluation for asynchronous concurrent systems
Bultan, T
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 441 - 455
[37] An AOP-Based Robot Behaviors Safety Checking Method
Ge, Binbin
Mao, Xinjun
Chen, Yin
Yang, Shuo
Yang, Shen
2015 INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS - COMPUTING TECHNOLOGY, INTELLIGENT TECHNOLOGY, INDUSTRIAL INFORMATION INTEGRATION (ICIICII), 2015, : 116 - 123
[38] Towards Integrating Statistical Model Checking into Property-Based Testing
Aichernig, Bernhard K.
Schumi, Richard
2016 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2016, : 71 - 76
[39] Verification method of security model based on UML and model checking
Cheng, Liang
Zhang, Yang
Jisuanji Xuebao/Chinese Journal of Computers, 2009, 32 (04): : 699 - 708
[40] Simultaneous SAT-based model checking of safety properties
Khasidashvili, Z
Nadel, A
Palti, A
Hanna, Z
HARDWARE AND SOFTWARE VERIFICATION AND TESTING, 2006, 3875 : 56 - 75

← 1 2 3 4 5 →