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.


Editor(s):
Ganty, Pierre
Loreti, Michele
Published in:
Proceedings of the 10th International Symposium on Trustworthy Global Computing, 147-162
Presented at:
10th International Symposium on Trustworthy Global Computing, Madrid, Spain, August 31- September 1, 2015
Year:
2015
Publisher:
Springer
Keywords:
Laboratories:




 Record created 2015-09-14, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)