Until recently, the state-of-the-art of Software Product Line (SPL) configuration and verification automation consisted of a collection of ad-hoc approaches tightly coupling a single input Variability Modeling Language (VML) with a single constraint solver. To remedy this situation, a novel generic model-driven architecture was then proposed that enables using a variety of VMLs and solvers. The key ideas of this proposal were (a) the use of a standard logical language (CLIF) as a pivot between VMLs and solvers, and (b) the use of a standard data exchange format (JSON) to explicilty and declaratively specify the abstract syntax and semantics of the VMLs to be used in an SPL engineering project and the automated reasoning task to be performed by the solvers.

Verifying and configuring large Software Product Lines (SPL) requires automation tools. Current state-of-the-art approaches involve translating variability models into a formalism accepted as input by a constraint solver. There are currently no standards for variability modeling languages (VML). There is also a variety of constraint solver input languages. This has resulted in a multiplication of ad-hoc architectures and tools specialized for a single pair of VML and solver, fragmenting the SPL community. To overcome this limitation, we propose a novel architecture based on model-driven code generation, where the syntax and semantics of VMLs can be declaratively specified as data, and a standard, human-readable, formal pivot language is used between the VML and the solver input language. This architecture is the first to be fully generic by being agnostic to both VML and the solver paradigm. To validate the genericity of the approach, we have implemented a prototype tool together with declarative specifications for the syntax and semantics of two different VMLs and two different solver families. One VML is for classic, static SPL, and the other for run-time reconfigurable dynamic SPL with soft constraints to be optimized during configuration. The two solver families are Constraint Satisfaction Programs (CSP) and Constraint Logic Programs (CLP).

With the popularity of software defined networking architectures, the growing complexity of its use cases dictates the need for better auditability especially for security. In this paper, we aim at facilitating high-level management-plane policy configuration conformance auditing and their reflection in the data plane, to detect missing or spurious flow rules with respect to security policies. To this end, we propose an efficient conformance checking approach based on an intentional northbound interface as well as traces of management, control and data plane. Leveraging a proof-of-concept implementation of our approach, we compare its conformance-checking runtime and precision against a direct method on virtual topologies and find that it significantly improves scalability. We conclude by proposing directions for further enhancements extending the techniques presented herein.