Verifying the safety properties of concurrent systems via simultaneous reachability.

• Main Author: Ozdemir, Kadir.
• Other Authors: Ural, Hasan
• Format: Others
• Published: University of Ottawa (Canada) 2009
• Subjects: Computer Science.
• Online Access: http://hdl.handle.net/10393/10294; http://dx.doi.org/10.20381/ruor-8220

This thesis proposes two techniques, simultaneous reachability analysis and simultaneous product method, to reduce the number of global states to be analyzed for verifying the safety properties of concurrent systems. Both techniques utilize the idea of simultaneous execution of transitions. Simultaneous reachability analysis is proposed for verifying a specific set of safety properties asserting absence of logical errors of communication protocols specified as a network of n ($n\ge 2$) processes communicating over error-free, bounded, FIFO queues, without placing any restrictions on the topology of the network and process structures. We prove that simultaneous reachability analysis not only verifies the absence of logical errors such as deadlock, nonexecutable transition, unspecified reception and buffer overflow (in a correct protocol) but also identifies every deadlock state, every nonexecutable transition, every missing receiving transition causing unspecified receptions and every channel at which a buffer overflow occurs (in an incorrect protocol). An empirical study is carried out to demonstrate the efficiency of simultaneous reachability analysis in terms of time and memory requirements. In this study, 300 protocols constructed by an automatic empirical protocol synthesizer are used and results are evaluated with respect to the characteristics of these protocols. Empirical results show that using simultaneous reachability analysis substantially reduces the number of global states. Simultaneous product method is proposed for verifying general safety properties of finite-state concurrent programs. In this method, a concurrent program is specified as a collection of processes represented by finite automata on finite words and the concurrent behavior of these processes is defined by usual operational semantics (CSP-style): actions that appear in several processes are synchronized, others are interleaved. Verification problem is formulated in the framework of automata-theoretic model-checking where the negation of a safety property is convened to a finite automaton on finite words and then an automaton is obtained by taking the simultaneous product of the automata representing processes and the automaton representing the negation of a safety property. We prove that any safety property for a finite-state concurrent program can be efficiently verified by using simultaneous product method.