Formal verification of cP systems using PAT3 and ProB

• DOI: 10.1007/s41965-020-00036-0
• Publication Date: 2020-03-26T16:04:36Z
• Authors: Yezhou Liu; Radu Nicolescu; Jing Sun
• Keywords: Liveness; Membrane Computing

As a recently proposed membrane computing model, cP systems are capable of solving computational hard and distributed problems. Although several membrane system variants were formally verified in previous research, none of their approaches was applicable to cP systems. To formally verify the safety and liveness properties of cP systems, we solve a famous NP-Complete problem—the subset sum problem—in cP systems and use the PAT3 and ProB model checkers to verify the cP solution. Our cP solution outperforms previous work in time complexity and uses fewer rules. To perform model checking in cP systems, we define several mapping rules from cP notation to formal verification languages CSP# and B. We show that we can use model checkers to effectively detect design errors in cP systems. This work is the first study on formal verification of cP systems, and it showed that cP models can be effectively transformed into model checking problems and verified automatically.