Formal Verification with Functional Indeterminacy on the Basis of Satisfiability Testing of the Conjunctive Normal Form

被引：2

作者：

Cheremisinova, L. D. ^{[1
]}

Novikov, D. Ya. ^{[1
]}

机构：

[1] Natl Acad Sci Belarus, United Inst Informat Problems, Ul Surganova 6, Minsk 220012, BELARUS

来源：

AUTOMATIC CONTROL AND COMPUTER SCIENCES | 2010年 / 44卷 / 01期

关键词：

computer-aided design; verification; CNF satisfiability;

D O I：

10.3103/S0146411610010013

中图分类号：

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

学科分类号：

0812 ;

摘要：

The verification problem for the case of the description of a functional indeterminacy set by a system of partially specified Boolean functions is considered. The formal approach based on the reduction of the verification problem to a satisfiability test of the conjunctive normal form is suggested. Three approaches to the solution of the verification problem based on sequential, simultaneous, and group testing of multi-output intervals of the system of partially specified Boolean functions are investigated.

引用

页码：1 / 10

页数：10

共 6 条

[1] Analysis of the Implementability of Descriptions with Functional Indeterminacy Based on the Verification of Conjunctive Normal Form Satisfiability
Novikov, D. Ya.
Cheremisinova, L. D.
AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2011, 45 (04) : 206 - 217
[2] The Incremental Satisfiability Problem for a Two Conjunctive Normal Form
De Ita Luna, Guillermo
Raymundo Marcial-Romero, J.
Hernandez, Jose A.
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 328 : 31 - 45
[3] An algorithm for the satisfiability problem of formulas in conjunctive normal form
Schuler, R
JOURNAL OF ALGORITHMS-COGNITION INFORMATICS AND LOGIC, 2005, 54 (01): : 40 - 44
[4] TO CHECKING SATISFIABILITY OF THE CONJUNCTIVE NORMAL-FORM OF THE BOOLEAN FUNCTION
ZAKREVSKY, AD
DOKLADY AKADEMII NAUK BELARUSI, 1994, 38 (04): : 5 - 7
[5] THE POLYNOMIAL COMPLEXITY OF CONJUNCTIVE NORMAL-FORM SATISFIABILITY, WHEN THE NUMBER OF CONJUNCTIONS AND NEGATIONS IS LIMITED
KOSSOVSKY, NK
PROKHOROFF, AB
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 620 : 241 - 245
[6] A Security Assurance Framework Combining Formal Verification and Security Functional Testing
Wang, Weiguang
Zeng, Qingkai
Mathur, Aditya P.
2012 12TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2012, : 136 - 139

← 1 →