Automatic Non-Interference Lemmas for Parameterized Model Checking

Parameterized model checking refers to any method that extends traditional, finite-state model checking to handle systems arbitrary number of processes. One popular approach to this problem uses abstraction and so-called guard strengthening. Here number of processes remain intact, while the rest are abstracted away. This initially causes counter-examples, but the user e non-interference lemmas, which eliminate spurious behavior by the abstracted processes. The technique is sound in that if the user writes a lemma that is not invariant, the proof will never succeed. Though the non-interference lemmas are typically much simpler than writing a full inductive invariant, there is still a non-trivial amount of human insight needed to analysis counter-examples and concoct the lemmas. In our work, we show how the process of inferring appropriate non-interference lemmas can be automated. oach is based on a very general theory that simply assumes a Galois connection between the concrete and abst...

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Jesse D. Bingham
• Keywords: FMCAD 2008, Formal Methods, Galois Connection, Non-interference Lemma, Parameterized Model Checking