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.

The feature interaction problem appears in many different kinds of complex systems, especially systems whose elements are created or maintained by separate entities - for example, a modern automobile that incorporates electronic systems produced by different suppliers. Cross-cutting concerns, such as safety and security, require a comprehensive analysis of the possible interactions. However, there is a combinatorial explosion in the number of feature combinations to be considered. Our work approaches the feature interaction problem from a novel point of view: we seek to use the abstract subject matter knowledge of domain experts to deduce why some features will NOT interact, rather than trying to discover or resolve the interactions. In this paper, we present a method that can automatically reduce the required number of combinations and situations that have to be evaluated or resolved for feature interactions. Our tool, called Morse, rules out feature combinations that cannot have interactions based on traceable deductions from relatively simple abstract requirements that capture relevant subject matter knowledge. Our method is useful as a means of focusing attention on particular situations where more detailed functional requirements may be needed to avoid unacceptable risk arising from unintended interactions between features. relatively simple abstract requirements that capture relevant subject matter knowledge. Our method is useful as a means of focusing attention on particular situations where more detailed functional requirements may be needed to avoid unacceptable risk arising from unintended interactions between features.

We propose to use model checking to detect feature interactions in a set of features under design for an automotive embedded system. In this paper, we present (1) the characteristics of the feature interaction problem in the automotive domain that make model checking an appropriate detection technique; (2) our proposal for a general, systematic definition of feature interactions for this domain based on the set of actuators in the vehicle influenced by the features; and (3) our solutions to two modelling issues that arise when creating a description in SMV of the behaviour of an integrated set of automotive features designed in MATLAB's STATEFLOW.

A novel approach to formal hardware verification results from the combination of symbolic trajectory evaluation and interactive theorem-pmviug.From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behavionr and timing.From interactive theorempmving we gain access to powerful mathematical tools such as induction and abstraction.We have prototype a hybrid tool and used this tool to obtain verification results that could not be easily obtained with previously published techniques.