Differential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL2 in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL, which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies.

Abstract Small round-off errors in safety-critical systems can lead to catastrophic consequences. In this context, determining if the result computed by a floating-point program is accurate enough with respect to its ideal real-number counterpart is essential. This paper presents PRECiSA 4.0, a tool that rigorously estimates the accumulated round-off error of a floating-point program. PRECiSA 4.0 combines static analysis, optimization techniques, and theorem proving to provide a modular approach for computing a provably correct round-off error estimation. PRECiSA 4.0 adds several features to previous versions of the tool that enhance its applicability and performance. These features include support for data collections such as lists, records, and tuples; support for recursion schemas; an updated floating-point formalization that closely characterizes the IEEE-754 standard; an efficient and modular analysis of function calls that improves the performances for large programs; and a new user interface integrated into Visual Studio Code.

Abstract The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate current state information, including position and velocity messages, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B protocol responsible for the encoding and decoding of aircraft positions. CPR is sensitive to computer arithmetic since it relies on functions that are intrinsically unstable such as floor and modulus. In this paper, a formal verification of the CPR algorithm is presented. In contrast to previous work, the algorithm presented here encompasses the entire range of message types supported by ADS-B. The paper also presents two implementations of the CPR algorithm, one in double-precision floating-point and one in 32-bit unsigned integers, which are both formally verified against the real-number algorithm. The verification proceeds in three steps. For each implementation, a version of CPR, which is simplified and manipulated to reduce numerical instability and leverage features of the datatypes, is proposed. Then, the Prototype Verification System (PVS) is used to formally prove real conformance properties, which assert that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify software conformance properties, which say that the software implementation of the improved algorithm is correct with respect to its idealized real-number counterpart. In concert, the two properties guarantee that the implementation meets the original specification. The two implementations will be included in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.

Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.

This paper presents a set of tools for mechanical reasoning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and Taylor's series expansions. Although the tools are designed for the proof assistant system PVS, expertise on PVS is not required. The ultimate goal of the tools is to provide guaranteed proofs of numerical properties with a minimal human-theorem prover interaction.

In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counter-example test inputs are then generated. The major problems of applying this approach to engineering applications derive from the fact that engineering programs have an infinite state space and non-linear numerical computations. Our solution is to combine predicate abstraction (which reduces the state space) with a numerical decision procedure (which supports predicate abstraction by solving non-linear constraints) based on interval analysis. We have developed a prototype and applied it to MC/DC (Modified Condition/Decision Coverage) test case generation. We have used the prototype on a number of C modules taken from a conflict detection and avoidance system and from a Boeing 737 autopilot simulator. The modules range from tens of lines up to thousands of lines in size. Our experience shows that although in theory the inclusion of a decision procedure for non-linear arithmetic may lead to non-terminating behavior and false positives (as abstraction-based model checking already does), our prototype is able to automatically produce feasible counterexamples with only a few exceptions. Furthermore, the process runs with acceptable execution times, without requiring any other knowledge of the specification, and without tampering with the original C programs.

A high level model of the concept of operations of NASA's Small Aircraft Transportation System for Higher Volume Operations (SATS-HVO) is presented. The model is a non-deterministic, asynchronous transition system. It provides a robust notion of safety that relies on the logic of the concept rather than on physical constraints such as aircraft performances. Several safety properties were established on this model. The modeling and verification effort resulted in the identification of 9 issues, including one major flaw, in the original concept. Ten recommendations were made to the SATS-HVO concept development working group. All the recommendations were accepted and incorporated into the current concept of operations. The model was written in PVS. The verification is performed using an explicit state exploration algorithm written and proven correct in PVS.

Explicit substitutions calculi are formal systems that implement /spl beta/-reduction by means of an internal substitution operator. In that calculi it is possible to delay the application of a substitution to a term or to consider terms with partially applied substitutions. The /spl lambda//sub /spl sigma//-calculus of explicit substitutions, proposed by M. Abadi et al. (1991), is a first-order rewriting system that implements substitution and renaming mechanism of /spl lambda/-calculus. However; /spl lambda//sub /spl sigma// does not preserve strong normalisation of /spl lambda/-calculus and it is not a confluent system. Typed variants of /spl lambda//sub /spl sigma// without composition are strongly normalising but not confluent, while variants with composition are confluent but do not preserve strong normalisation. Neither of them enjoys both properties. In this paper we propose the /spl lambda//sub /spl zeta//-calculus. This is, as far as we know, the first confluent calculus of explicit substitutions that preserves strong normalisation.