Product line (PL) engineering promotes the development of families of related products, where individual products are differentiated by which optional features they include. Modelling and analyzing requirements models of PLs allows for early detection and correction of requirements errors -- including unintended feature interactions, which are a serious problem in feature-rich systems. A key challenge in analyzing PL requirements is the efficient verification of the product family, given that the number of products is too large to be verified one at a time. Recently, it has been shown how the high-level design of an entire PL, that includes all possible products, can be compactly represented as a single model in the SMV language, and model checked using the NuSMV tool. The implementation in NuSMV uses BDDs, a method that has been outperformed by SAT-based algorithms. In this paper we develop PL model checking using two leading SAT-based symbolic model checking algorithms: IMC and IC3. We describe the algorithms, prove their correctness, and report on our implementation. Evaluating our methods on three PL models from the literature, we demonstrate an improvement of up to 3 orders of magnitude over the existing BDD-based method.

Scenarios and use cases are popular means of describing the intended system behaviour. They support a variety of features and, notably, allow for two different interpretations: existential and universal. These modalities allow a progressive shift from examples to general rules about the expected system behaviour. The combination of modalities in a scenario-based specification poses technical challenges when automated reasoning is to be provided. In particular, the use of conditional existential scenarios, of which use cases with preconditions are a common example, require reasoning in branching time. Yet, formally grounded approaches to requirements engineering and industrial verification approaches shy away from branching-time logics due to their relatively unintuitive semantics.

Web service applications are dynamic, highly distributed, and loosely coupled orchestrations of services which are notoriously difficult to debug. In this paper, we describe a user-guided recovery framework for web services. When behavioural correctness properties (safety and bounded liveness) of an application are violated at runtime, we automatically propose and rank recovery plans which users can then select for execution. For safety violations, such plans essentially involve "going back" -- compensating the occurred actions until an alternative behavior of the application is possible. For bounded liveness violations, such plans include both "going back" and "re-planning" --guiding the application towards a desired behavior. We report on the implementation and our experience with the recovery system.

Model checking is an automated technique for the verification of finite-state systems that is widely used in practice. In Bounded Model Checking (BMC) the system is checked only until a given execution depth from the initial state. State of the art model checkers apply Binary Decision Diagrams (BDDs) as well as Satisfiability Solving (SAT) for this task. However, both methods suffer from the state explosion problem, which restricts the application of model checking to only modestly sized systems. The importance of model checking makes it worthwhile to explore alternative technologies, in the hope of enabling the application of the technique to a wider class of systems. Description Logic (DL) is a family of knowledge representation formalisms, mainly used for designing ontologies, for which reasoning is based on tableaux techniques. In this article, we show how model checking problems can be solved using DL reasoning. We present two different encodings of a model checking problem as a consistency check in DL, and show how DL can serve as a natural setting for representing and solving a BMC problem. Experimental results, using the DL reasoner FaCT++, give encouraging results.

RuleBase is a formal verification tool, developed by the IBM Haifa Research Laboratory. It is the result of three years of experience in practical formal verification of hardware which, we believe, has been a key factor in bringing the tool to its current level of maturity. We present the tool, including several unique features, and summarize our usage experience.