Naslov
Exploring the Constraints in Formal Verification of Communication and Computing Systems

Autori
Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
IEEE MELECON 2002 Proceedings / Younis, Mohamed - Piscataway (NJ) : IEEE, The Institute of Electrical and Electronics Eng., 2002, 173-177

Skup
The 11th IEEE Mediterranean Electrotechnical Conference

Mjesto i datum
Kairo, Egipat, 07.05.2002. - 09.05.2002

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Formal methods ; Formal verification ; Model checking

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Elektrotehnika

POVEZANOST RADA