Sjef van Loo: Verifying SPLs using parity games expressing variability

Event Details

SPL verification can be costly when all the software products of an SPL are verified independently. It is well known that parity games can be used to verify software products. We propose a generalization of parity games, named variability parity games (VPGs), that encode multiple parity games in a single game graph decorated with edge labels expressing variability between the parity games. We show that a VPG can be constructed from a modal μ-calculus formula and an FTS that models the behaviour of the different software products of an SPL. Solving the resulting VPG decides for which products in the SPL the formula is satisfied. We introduce several algorithms to efficiently solve VPGs and exploit commonalities between the different parity games encoded. We perform experiments on SPL models to demonstrate that the VPG algorithms indeed outperform independently verifying every product in an SPL.