Engineering PapersSearch

Engineering topics

Thomas Pressburger

Publications and source records attributed to Thomas Pressburger.

Recommendations on Evidence and Process for Certification of Learning-enabled Components in Aerospace Systems

This report primarily identifies a collection of relevant and necessary evidence for assurance of machine learnt components (MLCs)—also known as learning-enabled components—integrated into aircraft systems, and gives preliminary suggestions on the elements of a certification process that invoke the identified evidence. The main focus is on feedforward neural networks that are static and trained offline through supervised learning. A brief background on the generic elements of the lifecycle of an MLC is given to contextualize the assurance considerations and, consequently, the evidence that is relevant and necessary to support certification. At the level of an MLC, those considerations relate to: (i) the consistency and correctness of MLC contributions to system functions in the context of a validated functional intent; and (ii) the absence of MLC contributions to aircraft-level failure conditions. At an ML model level, confidence in model and data properties contribute to assurance of the containing MLC, in particular: (a) generalizability and robustness of models, in the presence of inputs not previously seen during training, disturbances to inputs, and unexpected inputs; and (b) valid data, i.e., data that are at least representative, relevant, complete, and accurate. Evidence for the above span the elements of the ML lifecycle, and includes, at a minimum, lifecycle artifacts that pertain to: (1) properties of requirements capturing functional intent, safety constraints, and aspects of the intended use and operating environment; (2) model performance, model complexity and design, and algorithm choice; (3) achievement of required performance at the levels of a trained model during model development, a trained model after model development is complete, and a trained model that is transformed into an executable equivalent; (4) model implementation aspects necessary for transforming a trained model into the executable equivalent; (5) integration of the executable trained model into the containing MLC, and eventually the larger system; and, (6) lastly, the verification and validation (V&V) of each of the above. Such V&V lifecycle artifacts themselves include: aspects of coverage, e.g., of various levels of requirements by the input space of the model and the data; traceability (where applicable); application of formal methods for property specification, analysis, and checking. Examples of evidence generation methods and tools further ground the discussion on what constitutes evidence, and the contribution to assurance during certification. The identified assurance considerations and supporting evidence is not a comprehensive set. Additionally, neither what should be considered as sufficient evidence relative to the assigned criticality of an MLC, nor how criticality ought to be determined and adjusted, have been considered in this report. However, suggestions are made for potential activities of the ML lifecycle that are aimed at providing confidence that an MLC can be relied upon when integrated into its containing (aircraft) system. Those activities are proposed as candidate elements of a certification process for MLCs. The main purpose of this report to inform regulatory guidance and consensus standards that may be used to meet the safety intent of the applicable regulations.

Aviation safety

From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

FRET

Using FRET to Create, Analyze and Monitor Requirements for a Lift Plus Cruise Case Study

In this technical report we provide information on the use of the NASA Formal RequirementsElicitation Tool (FRET) to create requirements for a Lift Plus Cruise (LPC) aircraft case study. Furthermore, we provide details on using FRET to translate these requirements into an appropriate format for the Copilot tool, enabling their usage to perform runtime verification on a synthesized LPC system.

Formal Requirements Elicitation Tool

Wildfire-fighting Use Case Requirements to Monitor

In this technical report, we provide requirements for a wildfire-fighting use-case, towards the Safety Demonstrator 1. The use case will incorporate ground and airborne assets operating in a coordinated fashion, and will comprise five activities, from detection to the execution of the initial attack. Depending on the activity and the data involved, the requirements identified may be non-probabilistic or probabilistic. In both cases, we first identify some of the requirements we wish to monitor, and then present a formalization using the language of requirements of the NASA requirements elicitation tool FRET. To formalize probabilistic requirements, we use a novel extension to FRET’s requirements language that incorporates notions of probability, and discuss how requirements can be translated into existing probabilistic temporal logics like PCTL. We exemplify how some of the requirements presented can be monitored using the existing tools Ogma and Copilot. We close with a summary and future directions.

Requirements

Automated Verification of Programmable Logic Controller Programs Against Structured Natural Language Requirements

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

formal methods

Realizability Checking of Requirements in FRET

Requirements formalization has become increasingly popular in industrial settings as an effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis tools to prove important properties, such as consistency and realizability. In this report, we present the realizability analysis framework that we developed as part of the Formal Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of conflicts between requirements and simulation of counterexamples, and discuss results from industrial-level case studies.

Formal Requirements Elicitation Tool

Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (FRET), and the RV system Copilot. We extend FRET with mechanisms to capture additional information needed to generate monitors, and introduce OGMA, a new tool to bridge the gap between FRET and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our tool chain is available as open source.

FRET

Compositional Realizability Checking within FRET

A set of requirements for a reactive system is realizable if, for any sequence of inputs that satisfy the assumptions on the environment, the guarantees always hold. Realizability checking is essential to ensure that an implementation can be constructed that satisfies the requirements. We propose a framework that supports users in the non-trivial task of developing realizable requirements. Our framework uses architectural information to automatically de-compose a set of requirements into subsets that can be analyzed separately, and therefore more efficiently. It then integrates existing algorithms in order to detect unrealizability, identify minimal sets of conflicting requirements, and compute counterexamples. The capability to focus on minimal conflict sets is key for localizing and correcting the sources of unrealizability. Our approach supports this process by enabling users to interactively visualize and explore the produced conflict sets and counterexamples. We have implemented our framework in the open-source Formal Requirements Elicitation Tool (FRET), and have used it on a variety of industrial-level case studies, showcasing the strengths of our approach in terms of raw performance, as well as diagnostic potential.

FRET

The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained

Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulinkis a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOSIM are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.

Anastasia Mavridou

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems(ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods

From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET

Realizability checking refers to the formal procedure that aims to determine whether an implementation exists, always complying to a set of requirements, regardless of the stimuli provided by the system’s environment. Such a check is essential to ensure that the specification does not allow behavior that can force the system to violate safety constraints. In this paper, we present an approach that decomposes realizability checking into smaller, more tractable problems. More specifically, our approach automatically partitions specifications into sets of non-interfering requirements. We prove that checking whether a specification is realizable reduces to checking that each partition is realizable.We have integrated realizability checking and implemented our decomposition approach within the open-source Formal Requirements ElicitationTool (FRET). A FRET user may check the realizability of a specification monolithically or compositionally. We evaluate our approach by comparing monolithic and compositional checking and showcase the strengths of our decomposition approach on a variety of industrial-level case studies

Anastasia Mavridou

Authoring, Analyzing, and Monitoring Requirements for a Lift-Plus-Cruise Aircraft

Requirements specification and analysis is widely applied to ensure the correctness of industrial systems in safety critical domains. Requirements are often initially written in natural language, which is highly ambiguous, and as a second step transformed into a language with rigorous semantics for formal analysis. [Question/problem] In this paper, we report on our experience in requirements creation and analysis, as well as run-time monitor generation using the Formal Requirement Elicitation Tool (FRET), on an industrial case study for a Lift-Plus-Cruise concept aircraft. [Principal ideas/results] We study the creation of requirements directly in the structured language of FRET without a prior definition of the same requirements in natural language. We focus on requirements describing state machines and discuss the challenges that we faced, in terms of creating requirements and generating monitors. We demonstrate how realizability, i.e., checking whether a requirements specification can be implemented, is crucial for understanding temporal interdependencies among requirements. [Contribution] Our study is the first complete attempt at using FRET to create industrial, realizable requirements and generate run-time monitors. Insight from lessons learned was materialized into new features in the FRET and JKind analysis frameworks.

Requirements engineering

From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

FRET