Formal verification of cP systems using Coq

被引：2
|
作者：
Liu, Yezhou [1 ]
Nicolescu, Radu [1 ]
Sun, Jing [1 ]
机构：
[1] Univ Auckland, Sch Comp Sci, Auckland, New Zealand
来源：
JOURNAL OF MEMBRANE COMPUTING | 2021年 / 3卷 / 03期
关键词：
Membrane computing; P systems; cP systems; Formal verification; Theorem prover; Coq;
D O I：
10.1007/s41965-021-00080-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
P systems are widely used to solve computationally hard problems. In this study, we formally verify cP systems (P systems with complex objects) in the Coq proof assistant, and provide a corresponding open source library. To help transform cP notation into Gallina, we propose two sets of modelling guidelines. Comparing to existing P system formal verification studies, our approach shows many advantages and has great potential. To the best of our knowledge, this is the first study to formally verify membrane computing models using an interactive theorem prover.
引用
收藏
页码：205 / 220
页数：16
相关论文
共 50 条
  • [21] Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
    Bertot, Yves
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2018, 2018, 11187 : 3 - 10
  • [22] Formal verification of reconfigurable systems
    Rahim, Muhammad Abdul Basit Ur
    Raheem, Muhammad Ahsan Ur
    Sohail, Muhammad Khalid
    Farid, Mohammad Atif
    Mufti, Muhammad Rafiq
    SOFT COMPUTING, 2023,
  • [23] Formal verification of digital systems
    Swamy, G
    TENTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1997, : 213 - 217
  • [24] Formal verification of stabilizing systems
    Siegel, M
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 158 - 172
  • [25] On the formal verification of hybrid systems
    Guéguen, H
    Zaytoon, J
    CONTROL ENGINEERING PRACTICE, 2004, 12 (10) : 1253 - 1267
  • [26] Formal Verification of Cyberphysical Systems
    Michael, James Bret
    Drusinsky, Doron
    Wijesekera, Duminda
    COMPUTER, 2021, 54 (09) : 15 - 24
  • [27] Formal Verification of Automated Teller Machine Systems using SPIN
    Iqbal, Ikhwan Mohammad
    Adzkiya, Dieky
    Mukhlash, Imam
    INTERNATIONAL CONFERENCE ON MATHEMATICS: PURE, APPLIED AND COMPUTATION: EMPOWERING ENGINEERING USING MATHEMATICS, 2017, 1867
  • [28] Formal verification of infinite state systems using Boolean methods
    Bryant, Randal E.
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 1 - 3
  • [29] Formal verification of hybrid systems using CheckMate:: A case study
    Silva, BI
    Krogh, BH
    PROCEEDINGS OF THE 2000 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2000, : 1679 - 1683
  • [30] A hierarchical approach to the formal verification of embedded systems using MDGs
    Balakrishnan, S
    Tahar, S
    NINTH GREAT LAKES SYMPOSIUM ON VLSI, PROCEEDINGS, 1999, : 284 - 287
12345