Golok: Push-button Verification of Parameterized Systems

摘要: ion techniques include counter abstraction [German and Sistla 1992; Pnueli et al. 2002] environment [Clarke 2006; 2008]. The idea behind is to abstract process identities, where every state contains an denoting the number of processes in state. Environment closest our work. It follows a similar approach as abstraction; however, counting done for satisfying given predicate. An generated reference show all possible relations this can have with its environment; which closely related technique we compute maximal behavior that induce arbitrary environment. advantage these abstraction-based they verify class ACM Journal Name, Vol. V, No. N, March 2010. Golok: Push-button Verification Parameterized Systems · 29 parameterized systems do not currently cover: whose individual are necessarily finite-state such Lamport’s Bakery algorithm [Lamport 1974] Szymanski’s [Szymanski 1988]; typically either require human guidance obtaining appropriate or applicable certain restricted and/or properties (e.g., universal path properties). 8.2 Smart representation-based Techniques Another rely on smart representation mechanism based regular language [Bouajjani 2000; Abdulla 2002; 2007; Fisman 2008] graph-based [Saksena 2008; Baldan 2005; Llorens Oliver 2004] representations state-space system. These approaches verification safety/reachabil- ity systems. Recently, petri-net has been proposed 2007] tokens used denote pa- rameter system new logic, colored markings logic (CML), developed reason about petri-nets. work provides generic framework representing rameterized identifies fragment CML satisfiability problem decidable. Similar abstraction, some allow sys- tems infinite-state processes. On other hand, most provide algorithmic focus only one two classes while (but incomplete) works several classes. We also present implementation prove applicability. 8.3 Induction-based induction use network invariants reduce parameter- ized finite model checking [Wolper Lovinfosse 1990; Arons 2001; Clarke 1995]. find invariant I preserved by computation steps Therefore, if satisfies desired property specification φ then φ. generation usually requires man- ual guidance, cut-off fully automatic. [Pnueli 2001] computed automatically once relation provided. advantadge it covers bounded-data model; type clear how may be multi-parameterized 8.4 Cut-off Computation Closest solutions computing parameter [Emerson Namjoshi 1995; Emerson Kahlon 2003; 1996; Ball Yang Li 2010; Ip Dill Bingham Hu Siirtola 2010]. This aims equivalent one, finding k objective establish satisfied any (≥ k) [EmerACM 30 Hanna, Samuelson, Basu Rajan son 1995] values different types ring topology. In contrast above techniques, automatic, does depend specific independent communication topology sound but incomplete method takes input description terms standard input/output automata establishes value. While first time bound property; considering being verified cut-off, tighter obtained. For instance, using Namjoshi’s 1995], cannot enter critical section at same, size 4; value identified (token protocol) 2. short, topology, central theme develop applied 9. CONCLUSION AND FUTURE WORK correctness important prob- lem 2006]. Considering undecidable general [Apt Kozen 1986], heuristics solving subset scenarios equally problem. To end, shown effective existing approach, behavioral-automata com- position, automatic generating system, there exists more than unbounded communicate via both single-cast broadcast. Furthermore, effectively utilizing descriptions allows us obtain system-specific 14 out 15 cases were found lower previ- ously discovered bounds. A large extent, dictates space needs explored formal technique. systematic find- ing thus foundational advance towards improved scalability techniques. implemented tool, Golok, applicability Future includes extending theoretical practical treatment behavioral- composition explore expressive protocols cap- ture infinite-domain data. would sensible extract behavioral from common programming languages Golok real-world software 31