In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key system properties are supported by evidence (e.g., test results, proofs). Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), i.e., sets of software products with overlapping but distinct features and behaviours. Since SPLs can encompass very large numbers of products, developing a rigorous AC for each product individually is infeasible. Moreover, if the SPL evolves, e.g., by the modification or introduction of features, it can be infeasible to assess the impact of this change. Instead, the development and maintenance of ACs ought to be lifted such that a single AC can be developed for the entire SPL simultaneously, and be analyzed for regression in a variability-aware fashion. In this article, we describe a formal approach to lifted AC development and regression analysis. We formalize a language of variability-aware ACs for SPLs and study the lifting of template-based AC development. We also define a regression analysis to determine the effects of SPL evolutions on variability-aware ACs. We describe a model-based assurance management tool which implements these techniques, and illustrate our contributions by developing an AC for a product line of medical devices.

Assurance cases (AC) are structured arguments that justify why a system is acceptably safe. Though ACs can increase confidence that systems will operate safely and reliably, they are also susceptible to problems such as reasoning errors and confirmation bias. Recent work proposed AI-Supported Eliminative Argumentation (AI-EA), a framework leveraging Generative AI (GAI) models to support AC development by identifying potential reasons why the argument may be invalid (a.k.a. defeaters) so that they can be mitigated. However, this framework was not implemented and its effectiveness was not assessed empirically.In this practical experience paper, we implement AI-EA, explain and justify our design choices, and report on our practical experience in empirically evaluating its effectiveness in collaboration with experts in the safety domain. Our evaluation considers 171 AI-generated defeaters across two industrial case studies from the nuclear and automotive domains. Our findings show that GAI can generate informative defeaters with few significant hallucinations and that 25% of the generated defeaters were confirmed by developers of each AC to represent reasonable doubts or errors in the argument. Our implementation and data are made publicly available.

In recent decades, cyber-physical systems developed using Model-Driven Engineering (MDE) techniques have become ubiquitous in safety-critical domains. Safety assurance cases (ACs) are structured arguments designed to comprehensively show that such systems are safe; however, the reasoning steps, or strategies, used in AC arguments are often informal and difficult to rigorously evaluate. Consequently, AC arguments are prone to fallacies, and unsafe systems have been deployed as a result of fallacious ACs. To mitigate this problem, prior work [32] created a set of provably valid AC strategy templates to guide developers in building rigorous ACs. Yet instantiations of these templates remain error-prone and still need to be reviewed manually. In this paper, we report on using the interactive theorem prover Lean to bridge the gap between safety arguments and rigorous model-based reasoning. We generate formal, modelbased machine-checked AC arguments, taking advantage of the traceability between model and safety artifacts, and mitigating errors that could arise from manual argument assessment. The approach is implemented in an extended version of the MMINT-A model management tool [10]. Implementation includes a conversion of informal claims into formal Lean properties, decomposition into formal sub-properties and generation of correctness proofs. We demonstrate the applicability of the approach on two safety case studies from the literature.

Model-driven engineering (MDE) promotes automated model transformations along the entire development process. Guaranteeing the quality of early models is essential for a successful application of MDE techniques and related tool-supported model refinements. Do these models properly reflect the requirements elicited from the owners of the problem domain? Ultimately, this question needs to be asked to the domain experts. The problem is that a gap exists between the respective backgrounds of modeling experts and domain experts. MDE developers cannot show a model to the domain experts and simply ask them whether it is correct with respect to the requirements they had in mind. To facilitate their interaction and make such validation more systematic, we propose a methodology and a tool that derive a set of customizable questionnaires expressed in natural language from each model to be validated. Unexpected answers by domain experts help to identify those portions of the models requiring deeper attention. We illustrate the methodology and the current status of the developed tool MOTHIA, which can handle UML Use Case, Class, and Activity diagrams. We assess MOTHIA effectiveness in reducing the gap between domain and modeling experts, and in detecting modeling faults on the European Project CHOReOS.

Developers have to work with ever-present design-time uncertainty, i.e., Uncertainty about selecting among alternative design decisions. However, existing tools do not support working in the presence of uncertainty, forcing developers to either make provisional, premature decisions, or to avoid using the tools altogether until uncertainty is resolved. In this paper, we present a tool, called MU-MMINT, that allows developers to express their uncertainty within software artifacts and perform a variety of model management tasks such as reasoning, transformation and refinement in an interactive environment. In turn, this allows developers to defer the resolution of uncertainty, thus avoiding having to undo provisional decisions. See the companion video: http://youtu.be/kAWUm-iFatM.

Megamodels are often used in MDE to describe collections of models and relationships between them. Typical collection-based operations - map, reduce, filter - cannot be applied directly to megamodels since these operators need to take relationships between models into consideration. In this paper, we propose adapted versions of these operators, demonstrating them on four megamodeling scenarios. We then analyze their applicability for handling industrial-sized megamodels. Finally, we report on a reference implementation of the operators and experimental results using it.

Software product lines and model transformations are two techniques used in industry for managing the development of highly complex software. Product line approaches simplify the handling of software variants while model transformations automate software manipulations such as refactoring, optimization, code generation, etc. While these techniques are well understood independently, combining them to get the benefit of both poses a challenge because most model transformations apply to individual models while model-level product lines represent sets of models. In this paper, we address this challenge by providing an approach for automatically ``lifting'' model transformations so that they can be applied to product lines. We illustrate our approach using a case study and evaluate it through a set of experiments.

Requirements Engineering (RE) involves eliciting, understanding, and capturing system requirements, which naturally involves much uncertainty. During RE, analysts choose among alternative requirements, gradually narrowing down the system scope, and it is unlikely that all requirements uncertainties can be resolved before such decisions are made. There is a need for methods to support early requirements decision-making in the presence of uncertainty. We address this need by describing a novel technique for early decision-making and tradeoff analysis using goal models with uncertainty. The technique analyzes goal satisfaction over sets of models that can result from resolving uncertainty. Users make choices over possible analysis results, allowing our tool to find critical uncertainty reductions which must be resolved. An iterative methodology guides the resolution of uncertainties necessary to achieve desired levels of goal satisfaction, supporting trade-off analysis in the presence of uncertainty.