A state space abstract algorithm of incremental data recognition based on model checking

被引：0

作者：

Lang, Dapeng ^{[1
]}

Huang, Shaobin ^{[1
]}

Cheng, Yuan ^{[1
]}

Yang, Xinxin ^{[1
]}

Li, Ya ^{[1
]}

机构：

[1] College of Computer Sciences and Technology, Harbin Engineering University

来源：

Journal of Computational Information Systems | 2014年 / 10卷 / 04期

关键词：

Abstract; Formal verification; Incremental data; Model checking;

D O I：

10.12733/jcis9544

中图分类号：

学科分类号：

摘要：

Model checking has been widely used in hardware and software verification, but its state space explosion problem is still one of key issues limiting its applications in the industrial sector and popularity. In this paper, together with the practical application of incremental data extraction process, we use kripke structure to model the process. Then this paper uses the CTL logic formulas to represent the specifications that the model should satisfy. Based on the process above, we propose and implement a state-space abstraction algorithm so that the state transition diagrams will be merged into smaller ones in order to achieve the purposes of space reduction. It's proved that the method meets the purpose of reducing the number of states in the area of multi-process accessing to critical areas that are mutually constrained. And to some extend the method is universal. © 2014 Binary Information Press.

引用

页码：1731 / 1742

页数：11

共 10 条

[1]

Li D., Huang Y., Deng N., Formal verification of deadlock detection and advoidance in typed pi calculus, Journal of Computational Information Systems, 8, 2, pp. 819-829, (2012)

[2]

Bryant R.E., Graph-based algorithms for Boolean function manipulation, Computers, IEEE Transactions on, 100, 8, pp. 677-691, (1986)

[3]

Clarke E.M., Emerson E.A., Sistla A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), 8, 2, pp. 244-263, (1986)

[4]

Burch J.R., Clarke E.M., Long D., Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th ACM/IEEE Design Automation Conference, (1991)

[5]

Clarke E.M., Grumberg O., Long D.E., Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), 16, 5, pp. 1512-1542, (1994)

[6]

Emerson E.A., Temporal and modal logic, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995-1072, (1990)

[7]

[8]

Hedges L.V., Rhoads C.H., Correcting an analysis of variance for clustering, British Journal of Mathematical and Statistical Psychology, 64, pp. 20-37, (2011)

[9]

Clarke E.M., Emerson E.A., Design and synthesis of synchronization skeletons using branching time temporal logic, Proceedings of Logic of Programs, Lecture Notes in Computer Science, 131, pp. 52-71, (1981)

[10]

Pnueli A., A temporal logic of concurrent programs, Theoretical Computer Science, 13, pp. 45-60, (1981)

← 1 →