-
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.
-
Automatic generation and verification of test-stable floating-point code
Authors:
Laura Titolo,
Mariano Moscato,
Cesar A. Muñoz
Abstract:
Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numeri…
▽ More
Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numerical computations. Writing programs that take into consideration test instability is a difficult task that requires expertise on finite precision computations and rounding errors. This paper presents a toolchain to automatically generate and verify a provably correct test-stable floating-point program from a functional specification in real arithmetic. The input is a real-valued program written in the Prototype Verification System (PVS) specification language and the output is a transformed floating-point C program annotated with ANSI/ISO C Specification Language (ACSL) contracts. These contracts relate the floating-point program to its functional specification in real arithmetic. The transformed program detects if unstable tests may occur and, in these cases, issues a warning and terminate. An approach that combines the Frama-C analyzer, the PRECiSA round-off error estimator, and PVS is proposed to automatically verify that the generated program code is correct in the sense that, if the program terminates without a warning, it follows the same computational path as its real-valued functional specification.
△ Less
Submitted 7 January, 2020;
originally announced January 2020.
-
Eliminating Unstable Tests in Floating-Point Programs
Authors:
Laura Titolo,
Cesar A. Muñoz,
Marco A. Feliu,
Mariano M. Moscato
Abstract:
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in r…
▽ More
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.
△ Less
Submitted 30 November, 2018; v1 submitted 13 August, 2018;
originally announced August 2018.
-
Modeling Hybrid Systems in the Concurrent Constraint Paradigm
Authors:
Damián Adalid,
María del Mar Gallardo,
Laura Titolo
Abstract:
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contra…
▽ More
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contrast to the variable/value style typical of imperative languages. Several extensions of ccp have been proposed in order to model reactive systems. One of these extensions is the Timed Concurrent Constraint Language (tccp) that adds to ccp a notion of discrete time and new features to model time-out and preemption actions. The goal of this paper is to explore the expressive power of tccp to describe hybrid systems. We introduce the language Hy-tccp as a conservative extension of tccp, by adding a notion of continuous time and new constructs to describe the continuous dynamics of hybrid systems. In this paper, we present the syntax and the operational semantics of Hy-tccp together with some examples that show the expressive power of our new language.
△ Less
Submitted 8 January, 2015;
originally announced January 2015.
-
Modeling Hybrid Systems in Hy-tccp
Authors:
Damian Adalid,
Maria del Mar Gallardo,
Laura Titolo
Abstract:
Concurrent,reactive and hybrid systems require quality modeling languages to be described and analyzed. The Timed Concurrent Constraint Language (tccp) was introduced as a simple but powerful model for reactive systems. In this paper, we present hybrid tccp (hy-tccp), an extension of tccp over continuous time which includes new con- structs to model the continuous dynamics of hybrid systems.
Concurrent,reactive and hybrid systems require quality modeling languages to be described and analyzed. The Timed Concurrent Constraint Language (tccp) was introduced as a simple but powerful model for reactive systems. In this paper, we present hybrid tccp (hy-tccp), an extension of tccp over continuous time which includes new con- structs to model the continuous dynamics of hybrid systems.
△ Less
Submitted 15 December, 2014;
originally announced December 2014.
-
Abstract Diagnosis for tccp using a Linear Temporal Logic
Authors:
Marco Comini,
Laura Titolo,
Alicia Villanueva
Abstract:
Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge.
In this wor…
▽ More
Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge.
In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.
△ Less
Submitted 14 May, 2014;
originally announced May 2014.
-
Towards an Effective Decision Procedure for LTL formulas with Constraints
Authors:
Marco Comini,
Laura Titolo,
Alicia Villanueva
Abstract:
This paper presents an ongoing work that is part of a more wide-ranging project whose final scope is to define a method to validate LTL formulas w.r.t. a program written in the timed concurrent constraint language tccp, which is a logic concurrent constraint language based on the concurrent constraint paradigm of Saraswat. Some inherent notions to tccp processes are non-determinism, dealing with p…
▽ More
This paper presents an ongoing work that is part of a more wide-ranging project whose final scope is to define a method to validate LTL formulas w.r.t. a program written in the timed concurrent constraint language tccp, which is a logic concurrent constraint language based on the concurrent constraint paradigm of Saraswat. Some inherent notions to tccp processes are non-determinism, dealing with partial information in states and the monotonic evolution of the information. In order to check an LTL property for a process, our approach is based on the abstract diagnosis technique. The concluding step of this technique needs to check the validity of an LTL formula (with constraints) in an effective way.
In this paper, we present a decision method for the validity of temporal logic formulas (with constraints) built by our abstract diagnosis technique.
△ Less
Submitted 19 August, 2013;
originally announced August 2013.
-
Abstract Diagnosis for Timed Concurrent Constraint programs
Authors:
Marco Comini,
Laura Titolo,
Alicia Villanueva
Abstract:
The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency. In this paper, we provide a general framework for the debugging…
▽ More
The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency. In this paper, we provide a general framework for the debugging of tccp programs. To this end, we first present a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems. We also provide an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation. Given a tccp program and a behavior specification, our debugging approach automatically detects whether the program satisfies the specification. This differs from other semiautomatic approaches to debugging and avoids the need to provide symptoms in advance. We show the efficacy of our approach by introducing two illustrative examples. We choose a specific abstract domain and show how we can detect that a program is erroneous.
△ Less
Submitted 7 September, 2011;
originally announced September 2011.
