Skip to content

ProVeLines

ProVeLines is a Product line of Verifiers for software product Lines. It constitutes the result of three-year-long research work on product-line model checking. As a product line, ProVeLines is composed of several variants built from the same code base. Every variant implements specific model checking procedures. They all share a common input language, fPromela, which is an extension of Promela. Features referenced in an fPromela model must first be declared in a TVL model.

Variability within ProVeLines comes from four factors: the type of system, the properties to check, the complexity of features, and the used data structures. At the moment, it can verify purely discrete systems and real-time systems only, that is, Featured Transition Systems and Featured Timed Automata respectively. It can perform three computations: reachability, (stutter) F-simulation, and LTL formula checking. If real-time models are considered, only reachability is possible. In addition to purely Boolean features, ProVeLines supports Multi-Features and Numeric Features. Finally, ProVeLines provides three alternatives to represent and check feature formulae: binary decision diagrams (more precisely, the CuDD library), boolean formula in conjunctive normal form (used together with the MiniSat solver), and abstract syntax tree (as implemented in Microsoft’s Z3). SNIP, our previous model checking tool, is but one variant of ProVeLines with support for LTL verification of purely boolean, discrete software product lines, and equipped with binary decision diagrams.

To get more detailed information about ProVeLines, please follow the following links: