Wang, QiangBliudze, Simon2015-09-142015-09-142015-09-14201510.1007/978-3-319-28766-9_10https://infoscience.epfl.ch/handle/20.500.14299/117804This 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.Formal verificationPredicate AbstractionPartial Order ReductionBIPtext::conference output::conference proceedings::conference paper