TY - CHAP

T1 - Brief announcement: MP-state

T2 - State-aware software model checking of message-passing systems

AU - Muftuoglu, C.A.

AU - Bokor, P.

AU - Suri, Neeraj

PY - 2012

Y1 - 2012

N2 - Software model checking [4] is a useful and practical branch of verification for verifying the implementation of the system. The wide usability comes at a price of low time and space efficiency. In fact, model checking of even simple single-process programs can take several hours using state-of-the-art techniques [6]. Verification complexity gets even worse for concurrent programs that simultaneously execute loosely coupled processes. Verification efficiency can be greatly improved by capturing the state of the program, a technique generally referred to as stateful model checking [2]. Intuitively, state capture enables to detect that two states are identical and, therefore, to consider only a representative state for verification. Unfortunately, capturing the state in general software systems can be very hard, even if the entire state of the system resides in the (local) memory. As a result, certain verification approaches (commonly called stateless model checking) do not capture the system's state at all [4]. Stateful model checking is in principle possible for software, however, at a price of considerable overhead. Therefore, stateful model checking is efficient only if the achieved reduction of redundantly explored states compensate for the overhead. © 2012 Springer-Verlag.

AB - Software model checking [4] is a useful and practical branch of verification for verifying the implementation of the system. The wide usability comes at a price of low time and space efficiency. In fact, model checking of even simple single-process programs can take several hours using state-of-the-art techniques [6]. Verification complexity gets even worse for concurrent programs that simultaneously execute loosely coupled processes. Verification efficiency can be greatly improved by capturing the state of the program, a technique generally referred to as stateful model checking [2]. Intuitively, state capture enables to detect that two states are identical and, therefore, to consider only a representative state for verification. Unfortunately, capturing the state in general software systems can be very hard, even if the entire state of the system resides in the (local) memory. As a result, certain verification approaches (commonly called stateless model checking) do not capture the system's state at all [4]. Stateful model checking is in principle possible for software, however, at a price of considerable overhead. Therefore, stateful model checking is efficient only if the achieved reduction of redundantly explored states compensate for the overhead. © 2012 Springer-Verlag.

KW - Concurrent program

KW - Coupled process

KW - Message passing systems

KW - Software model checking

KW - Software systems

KW - Space efficiencies

KW - Two-state

KW - Verification complexity

KW - Message passing

KW - Network security

KW - Stabilization

KW - Model checking

U2 - 10.1007/978-3-642-33536-5_18

DO - 10.1007/978-3-642-33536-5_18

M3 - Chapter

SN - 9783642335358

VL - 7596 LNCS

SP - 183

EP - 186

BT - Stabilization, Safety, and Security of Distributed Systems

ER -