-
A Compositional Proof Framework for FRETish Requirements
Authors:
Esther Conrad,
Laura Titolo,
Dimitra Giannakopoulou,
Thomas Pressburger,
Aaron Dutle
Abstract:
Structured natural languages provide a trade space between ambiguous natural languages that make up most written requirements and mathematical formal specifications such as Linear Temporal Logic. FRETish is a structured natural language for the elicitation of system requirements developed at NASA. The related open-source tool Fret provides support for translating FRETish requirements into temporal…
▽ More
Structured natural languages provide a trade space between ambiguous natural languages that make up most written requirements and mathematical formal specifications such as Linear Temporal Logic. FRETish is a structured natural language for the elicitation of system requirements developed at NASA. The related open-source tool Fret provides support for translating FRETish requirements into temporal logic formulas that can be input to several verification and analysis tools. In the context of safety-critical systems, it is crucial to ensure that a generated formula captures the semantics of the corresponding FRETish requirement precisely. This paper presents a rigorous formalization of the FRETish language including a new denotational semantics and a proof of semantic equivalence between FRETish specifications and their temporal logic counterparts computed by Fret. The complete formalization and the proof have been developed in the Prototype Verification System (PVS) theorem prover.
△ Less
Submitted 10 January, 2022;
originally announced January 2022.
-
From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project
Authors:
Aaron Dutle,
César Muñoz,
Esther Conrad,
Alwyn Goodloe,
Laura Titolo,
Ivan Perez,
Swee Balachandran,
Dimitra Giannakopoulou,
Anastasia Mavridou,
Thomas Pressburger
Abstract:
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 requ…
▽ More
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.
△ Less
Submitted 2 December, 2020;
originally announced December 2020.
-
Verifying the Safety of a Flight-Critical System
Authors:
Guillaume Brat,
David Bushnell,
Misty Davies,
Dimitra Giannakopoulou,
Falk Howar,
Temesghen Kahsai
Abstract:
This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal veri…
▽ More
This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.
△ Less
Submitted 9 February, 2015;
originally announced February 2015.
-
Proceedings 1st Workshop on Formal Integrated Development Environment
Authors:
Catherine Dubois,
Dimitra Giannakopoulou,
Dominique Méry
Abstract:
This volume contains the proceedings of F-IDE 2014, the first international workshop on Formal Integrated Development Environment, which was held as an ETAPS 2014 satellite event, on April 6, 2014, in Grenoble (France). High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an…
▽ More
This volume contains the proceedings of F-IDE 2014, the first international workshop on Formal Integrated Development Environment, which was held as an ETAPS 2014 satellite event, on April 6, 2014, in Grenoble (France). High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs. Thus tools are needed for handling specifications, program constructs and verification artifacts. The aim of the F-IDE workshop is to provide a forum for presenting and discussing research efforts as well as experience returns on design, development and usage of formal IDE aiming at making formal methods "easier" for both specialists and non-specialists.
△ Less
Submitted 23 April, 2014;
originally announced April 2014.
-
Abstraction and Learning for Infinite-State Compositional Verification
Authors:
Dimitra Giannakopoulou,
Corina S. Păsăreanu
Abstract:
Despite many advances that enable the application of model checking techniques to the verification of large systems, the state-explosion problem remains the main challenge for scalability. Compositional verification addresses this challenge by decomposing the verification of a large system into the verification of its components. Recent techniques use learning-based approaches to automate composit…
▽ More
Despite many advances that enable the application of model checking techniques to the verification of large systems, the state-explosion problem remains the main challenge for scalability. Compositional verification addresses this challenge by decomposing the verification of a large system into the verification of its components. Recent techniques use learning-based approaches to automate compositional verification based on the assume-guarantee style reasoning. However, these techniques are only applicable to finite-state systems. In this work, we propose a new framework that interleaves abstraction and learning to perform automated compositional verification of infinite-state systems. We also discuss the role of learning and abstraction in the related context of interface generation for infinite-state components.
△ Less
Submitted 19 September, 2013;
originally announced September 2013.
