assurance case
Towards Continuous Assurance with Formal Verification and Assurance Cases
Abeywickrama, Dhaminda B., Fisher, Michael, Wheeler, Frederic, Dennis, Louise
Autonomous systems must sustain justified confidence in their correctness and safety across their operational lifecycle-from design and deployment through post-deployment evolution. Traditional assurance methods often separate development-time assurance from runtime assurance, yielding fragmented arguments that cannot adapt to runtime changes or system updates - a significant challenge for assured autonomy. Towards addressing this, we propose a unified Continuous Assurance Framework that integrates design-time, runtime, and evolution-time assurance within a traceable, model-driven workflow as a step towards assured autonomy. In this paper, we specifically instantiate the design-time phase of the framework using two formal verification methods: RoboChart for functional correctness and PRISM for probabilistic risk analysis. We also propose a model-driven transformation pipeline, implemented as an Eclipse plugin, that automatically regenerates structured assurance arguments whenever formal specifications or their verification results change, thereby ensuring traceability. We demonstrate our approach on a nuclear inspection robot scenario, and discuss its alignment with the Trilateral AI Principles, reflecting regulator-endorsed best practices.
- North America > United States > District of Columbia > Washington (0.04)
- Europe > United Kingdom > England > Greater Manchester > Manchester (0.04)
- Europe > United Kingdom > England > Cheshire > Warrington (0.04)
- Europe > Italy > Marche > Ancona Province > Ancona (0.04)
- Government > Regional Government (0.46)
- Energy > Power Industry (0.46)
- Information Technology > Security & Privacy (0.46)
ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Vin, Eric, Miller, Kyle A., Incer, Inigo, Seshia, Sanjit A., Fremont, Daniel J.
Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces ScenicProver, a verification framework that aims to fill this gap. Built upon the Scenic probabilistic programming language, the framework supports: (1) compositional system description with clear component interfaces, ranging from interpretable code to black boxes; (2) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (3) evidence generation through testing, formal proofs via Lean 4 integration, and importing external assumptions; (4) systematic combination of generated evidence using contract operators; and (5) automatic generation of assurance cases tracking the provenance of system-level guarantees. We demonstrate the framework's effectiveness through a case study on an autonomous vehicle's automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for radar and laser sensors and focusing testing efforts on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.
- North America > United States > Michigan > Washtenaw County > Ann Arbor (0.14)
- North America > United States > California > Santa Cruz County > Santa Cruz (0.14)
- North America > United States > California > Alameda County > Berkeley (0.14)
- (5 more...)
Explainable Compliance Detection with Multi-Hop Natural Language Inference on Assurance Case Structure
Ikhwantri, Fariz, Marijan, Dusica
Ensuring complex systems meet regulations typically requires checking the validity of assurance cases through a claim-argument-evidence framework. Some challenges in this process include the complicated nature of legal and technical texts, the need for model explanations, and limited access to assurance case data. We propose a compliance detection approach based on Natural Language Inference (NLI): EXplainable CompLiance detection with Argumentative Inference of Multi-hop reasoning (EXCLAIM). We formulate the claim-argument-evidence structure of an assurance case as a multi-hop inference for explainable and traceable compliance detection. We address the limited number of assurance cases by generating them using large language models (LLMs). We introduce metrics that measure the coverage and structural consistency. We demonstrate the effectiveness of the generated assurance case from GDPR requirements in a multi-hop inference task as a case study. Our results highlight the potential of NLI-based approaches in automating the regulatory compliance process.
- North America > United States > Minnesota > Hennepin County > Minneapolis (0.14)
- North America > Dominican Republic (0.04)
- Europe > Norway > Eastern Norway > Oslo (0.04)
- (9 more...)
- Law (1.00)
- Information Technology > Security & Privacy (1.00)
- Government (1.00)
Explaining Unreliable Perception in Automated Driving: A Fuzzy-based Monitoring Approach
Salvi, Aniket, Weiss, Gereon, Trapp, Mario
Autonomous systems that rely on Machine Learning (ML) utilize online fault tolerance mechanisms, such as runtime monitors, to detect ML prediction errors and maintain safety during operation. However, the lack of human-interpretable explanations for these errors can hinder the creation of strong assurances about the system's safety and reliability. This paper introduces a novel fuzzy-based monitor tailored for ML perception components. It provides human-interpretable explanations about how different operating conditions affect the reliability of perception components and also functions as a runtime safety monitor. We evaluated our proposed monitor using naturalistic driving datasets as part of an automated driving case study. The interpretability of the monitor was evaluated and we identified a set of operating conditions in which the perception component performs reliably. Additionally, we created an assurance case that links unit-level evidence of \textit{correct} ML operation to system-level \textit{safety}. The benchmarking demonstrated that our monitor achieved a better increase in safety (i.e., absence of hazardous situations) while maintaining availability (i.e., ability to perform the mission) compared to state-of-the-art runtime ML monitors in the evaluated dataset.
- Europe > Germany > Bavaria > Upper Bavaria > Munich (0.04)
- Europe > Finland > Southwest Finland > Turku (0.04)
- Automobiles & Trucks (1.00)
- Transportation > Ground > Road (0.85)
- Information Technology > Robotics & Automation (0.71)
- Information Technology > Artificial Intelligence > Robots > Autonomous Vehicles (0.71)
- Information Technology > Artificial Intelligence > Representation & Reasoning > Uncertainty > Fuzzy Logic (0.70)
- Information Technology > Artificial Intelligence > Machine Learning > Performance Analysis > Accuracy (0.46)
A Framework for the Assurance of AI-Enabled Systems
Kapusta, Ariel S., Jin, David, Teague, Peter M., Houston, Robert A., Elliott, Jonathan B., Park, Grace Y., Holdren, Shelby S.
The United States Department of Defense (DOD) looks to accelerate the development and deployment of AI capabilities across a wide spectrum of defense applications to maintain strategic advantages. However, many common features of AI algorithms that make them powerful, such as capacity for learning, large-scale data ingestion, and problem-solving, raise new technical, security, and ethical challenges. These challenges may hinder adoption due to uncertainty in development, testing, assurance, processes, and requirements. Trustworthiness through assurance is essential to achieve the expected value from AI. This paper proposes a claims-based framework for risk management and assurance of AI systems that addresses the competing needs for faster deployment, successful adoption, and rigorous evaluation. This framework supports programs across all acquisition pathways provide grounds for sufficient confidence that an AI-enabled system (AIES) meets its intended mission goals without introducing unacceptable risks throughout its lifecycle. The paper's contributions are a framework process for AI assurance, a set of relevant definitions to enable constructive conversations on the topic of AI assurance, and a discussion of important considerations in AI assurance. The framework aims to provide the DOD a robust yet efficient mechanism for swiftly fielding effective AI capabilities without overlooking critical risks or undermining stakeholder trust.
- North America > United States > Virginia > Fairfax County > McLean (0.04)
- North America > United States > Maryland > Prince George's County > Laurel (0.04)
- North America > United States > District of Columbia > Washington (0.04)
- Workflow (0.47)
- Research Report (0.40)
- Government > Regional Government > North America Government > United States Government (1.00)
- Government > Military (1.00)
E-LENS: User Requirements-Oriented AI Ethics Assurance
Despite the much proliferation of AI ethical principles in recent years, there is a challenge of assuring AI ethics with current AI ethics frameworks in real-world applications. While system safety has emerged as a distinct discipline for a long time, originated from safety concerns in early aircraft manufacturing. The safety assurance is now an indispensable component in safety critical domains. Motivated by the assurance approaches for safety-critical systems such as aviation, this paper introduces the concept of AI ethics assurance cases into the AI ethics assurance. Three pillars of user requirements, evidence, and validation are proposed as key components and integrated into AI ethics assurance cases for a new approach of user requirements-oriented AI ethics assurance. The user requirements-oriented AI ethics assurance case is set up based on three pillars and hazard analysis methods used in the safety assurance of safety-critical systems. This paper also proposes a platform named Ethical-Lens (E-LENS) to implement the user requirements-oriented AI ethics assurance approach. The proposed user requirements-based E-LENS platform is then applied to assure AI ethics of an AI-driven human resource shortlisting system as a case study to show the effectiveness of the proposed approach.
- North America > United States (1.00)
- Oceania > Australia (0.46)
- Europe > Belgium (0.14)
- Asia (0.14)
- Information Technology > Security & Privacy (0.93)
- Law (0.93)
- Government > Regional Government > North America Government > United States Government (0.67)
Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems
Abeywickrama, Dhaminda B., Fisher, Michael, Wheeler, Frederic, Dennis, Louise
This report provides an overview of the workshop titled Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems, hosted by the Centre for Robotic Autonomy in Demanding and Long-Lasting Environments (CRADLE) on September 2, 2024, at The University of Manchester, UK. The event brought together representatives from six regulatory and assurance bodies across diverse sectors to discuss challenges and evidence for ensuring the safety of autonomous and robotic systems, particularly autonomous inspection robots (AIR). The workshop featured six invited talks by the regulatory and assurance bodies. CRADLE aims to make assurance an integral part of engineering reliable, transparent, and trustworthy autonomous systems. Key discussions revolved around three research questions: (i) challenges in assuring safety for AIR; (ii) evidence for safety assurance; and (iii) how assurance cases need to differ for autonomous systems. Following the invited talks, the breakout groups further discussed the research questions using case studies from ground (rail), nuclear, underwater, and drone-based AIR. This workshop offered a valuable opportunity for representatives from industry, academia, and regulatory bodies to discuss challenges related to assured autonomy. Feedback from participants indicated a strong willingness to adopt a design-for-assurance process to ensure that robots are developed and verified to meet regulatory expectations.
- Europe > United Kingdom > England > Greater Manchester > Manchester (0.25)
- North America > United States > Massachusetts (0.04)
- Europe > United Kingdom > England > Cheshire > Warrington (0.04)
- Research Report (1.00)
- Instructional Material > Course Syllabus & Notes (0.54)
- Law (1.00)
- Government > Military (1.00)
- Transportation > Ground > Rail (0.68)
Where AI Assurance Might Go Wrong: Initial lessons from engineering of critical systems
Bloomfield, Robin, Rushby, John
We draw on our experience working on system and software assurance and evaluation for systems important to society to summarise how safety engineering is performed in traditional critical systems, such as aircraft flight control. We analyse how this critical systems perspective might support the development and implementation of AI Safety Frameworks. We present the analysis in terms of: system engineering, safety and risk analysis, and decision analysis and support. We consider four key questions: What is the system? How good does it have to be? What is the impact of criticality on system development? and How much should we trust it? We identify topics worthy of further discussion. In particular, we are concerned that system boundaries are not broad enough, that the tolerability and nature of the risks are not sufficiently elaborated, and that the assurance methods lack theories that would allow behaviours to be adequately assured. We advocate the use of assurance cases based on Assurance 2.0 to support decision making in which the criticality of the decision as well as the criticality of the system are evaluated. We point out the orders of magnitude difference in confidence needed in critical rather than everyday systems and how everyday techniques do not scale in rigour. Finally we map our findings in detail to two of the questions posed by the FAISC organisers and we note that the engineering of critical systems has evolved through open and diverse discussion. We hope that topics identified here will support the post-FAISC dialogues.
- Europe > Austria > Vienna (0.14)
- Europe > United Kingdom > England > Cambridgeshire > Cambridge (0.14)
- Asia > South Korea > Seoul > Seoul (0.05)
- (14 more...)
- Transportation > Air (1.00)
- Health & Medicine (1.00)
- Energy > Power Industry > Utilities > Nuclear (1.00)
- Government > Regional Government (0.93)
Landscape of AI safety concerns -- A methodology to support safety assurance for AI-based autonomous systems
Schnitzer, Ronald, Kilian, Lennart, Roessner, Simon, Theodorou, Konstantinos, Zillner, Sonja
Artificial Intelligence (AI) has emerged as a key technology, driving advancements across a range of applications. Its integration into modern autonomous systems requires assuring safety. However, the challenge of assuring safety in systems that incorporate AI components is substantial. The lack of concrete specifications, and also the complexity of both the operational environment and the system itself, leads to various aspects of uncertain behavior and complicates the derivation of convincing evidence for system safety. Nonetheless, scholars proposed to thoroughly analyze and mitigate AI-specific insufficiencies, so-called AI safety concerns, which yields essential evidence supporting a convincing assurance case. In this paper, we build upon this idea and propose the so-called Landscape of AI Safety Concerns, a novel methodology designed to support the creation of safety assurance cases for AI-based systems by systematically demonstrating the absence of AI safety concerns. The methodology's application is illustrated through a case study involving a driverless regional train, demonstrating its practicality and effectiveness.
- Research Report (0.50)
- Overview (0.46)
- Transportation > Ground > Rail (0.47)
- Information Technology > Security & Privacy (0.46)
Towards Assurance of LLM Adversarial Robustness using Ontology-Driven Argumentation
Momcilovic, Tomas Bueno, Buesser, Beat, Zizzo, Giulio, Purcell, Mark, Balta, Dian
Despite the impressive adaptability of large language models (LLMs), challenges remain in ensuring their security, transparency, and interpretability. Given their susceptibility to adversarial attacks, LLMs need to be defended with an evolving combination of adversarial training and guardrails. However, managing the implicit and heterogeneous knowledge for continuously assuring robustness is difficult. We introduce a novel approach for assurance of the adversarial robustness of LLMs based on formal argumentation. Using ontologies for formalization, we structure state-of-the-art attacks and defenses, facilitating the creation of a human-readable assurance case, and a machine-readable representation. We demonstrate its application with examples in English language and code translation tasks, and provide implications for theory and practice, by targeting engineers, data scientists, users, and auditors.
- Europe > Switzerland > Zürich > Zürich (0.14)
- Europe > Middle East > Malta > Port Region > Southern Harbour District > Valletta (0.04)
- Europe > Ireland > Leinster > County Dublin > Dublin (0.04)
- Europe > Germany > Bavaria > Upper Bavaria > Munich (0.04)
- Information Technology > Artificial Intelligence > Representation & Reasoning > Ontologies (1.00)
- Information Technology > Artificial Intelligence > Natural Language > Large Language Model (1.00)
- Information Technology > Artificial Intelligence > Machine Learning > Neural Networks > Deep Learning (0.69)