Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction
This paper presents a novel safety property verification approach for component-based systems
modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation
with data transfer and priority. Our contributions consist of: (1) an on-the-fly lazy predicate
abstraction technique for BIP; (2) a novel explicit state reduction technique, called simultaneous
set reduction, that can be combined with lazy predicate abstraction to prune the search space
of abstract reachability analysis; (3) a prototype tool implementing all the proposed techniques.
We also conduct thorough experimental evaluation, which demonstrates the effectiveness of our
proposed approach.
bipchecker.pdf
openaccess
555.91 KB
Adobe PDF
e5a4fcd0b5325585a483ce322d338936