Formal verification of concurrent software: two case studies

Hana Chockler, Eitan Farchi, Ziv Glazberg, Benny Godlin, Yarden Nir-Buchbinder, Ishai Rabinovitz

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

2 Citations (Scopus)

Abstract

Software model checking came to the focus of research recently, with sharp growth in the number of safety-critical applications and in the complexity of software. In model checking of software we meet some obstacles which do not exist in model checking of hardware: the state explosion problem is more acute, the model often consists of many processes that run concurrently, and there also can be a requirement for correct behavior in the presence of failures. Also, the programs are written in high-level programming languages, which causes two problems: the model-checker has to understand a programming language,and the state space of the program can be infinite (for example, the range of values for integer values is infinite in theory). In this paper, we present two case studies of real projects at IBM, which were formally modeled and verified using ExpliSAT model checker, as well a testing tool ConTest. The second case also involves modeling limited Byzantine (malicious) failures of processes. We discuss the special structure of the control flow graph of these programs and perform probabilistic analysis of the number of random executions needed in order to execute all control flow paths with high probability. We also compare the performance of ConTest and ExpliSAT on these case studies.
Original languageEnglish
Title of host publicationProceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD)
PublisherACM
Publication statusPublished - 17 Jul 2006

Fingerprint

Dive into the research topics of 'Formal verification of concurrent software: two case studies'. Together they form a unique fingerprint.

Cite this