Exploring the Constraints in Formal Verification of Communication and Computing Systems (CROSBI ID 483432)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Bogunović, Nikola
engleski
Exploring the Constraints in Formal Verification of Communication and Computing Systems
The high cost of correcting errors in digital design and communication protocols of e-economy systems calls for creative formal verification methods. Unlike testing and simulation, formal verification methods cover the entire system state space and all possible combination of inputs. There are two common approaches to the problem of formal verification: theorem proving and model checking. Since the deductive approach in theorem proving has many noted shortcomings the focus of the paper is on the model checking techniques. The paper explores the constraints of the application of the verification process, finds the most difficult steps in terms of space and time complexity and proposes the necessary operations to strengthen the methodology and expand it to real-world sized examples. The state explosion problem is tackled by applying BDD diagrams that can efficiently represent relations (functions) and sets. Finally, the paper suggests some general research directions that are likely to lead to technological advances.
Formal methods ; Formal verification ; Model checking
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
173-177.
2002.
objavljeno
Podaci o matičnoj publikaciji
IEEE MELECON 2002 Proceedings
Younis, Mohamed
Piscataway (NJ): IEEE, The Institute of Electrical and Electronics Eng.
Podaci o skupu
The 11th IEEE Mediterranean Electrotechnical Conference
predavanje
07.05.2002-09.05.2002
Kairo, Egipat