LfSA on Thursday, July 15th

09:00‑10:00 Invited Talk
Location: AT 2.12
09:00 Thomas A. Henzinger (IST Austria)
The Quantitative Agenda in System Analysis
10:30‑12:30 Session 1
Location: AT 2.12
10:30 Christian Engel and Peter Schmitt
A Formalization of the RTSJ Scoped Memory Model in Dynamic Logic

The Real-Time Specification for Java (RTSJ) features a region-based memory model with the capability to explicitly free memory regions (so called scoped memory areas). For preventing dangling references it introduces runtime checks, raising errors in the case of a failure, to restrict the creation of references between objects residing in different regions. This work presents an operational semantics for the RTSJ memory model formulated in a sequent calculus for dynamic logic. The calculus employs symbolic execution and can be used for proving the absence of failed runtime checks. This is crucial for giving safety guarantees for RTSJ applications or could allow an RTSJ compliant Java Virtual Machine (JVM) to skip this kind of runtime checks resulting in improved performance. The presented approach has been implemented in the KeY system and evaluated for its practical feasibility.

11:00 Alessandro Cimatti, Marco Roveri and Stefano Tonetta
Requirements Validation for Hybrid Systems

The importance of requirements for the whole development flow calls for strong validation techniques based on formal methods. % In the case of discrete systems, some approaches based on temporal logic satisfiability are gaining increasing momentum. % However, in many real-world domains (e.g. railways signaling), the requirements constrain the temporal evolution of both discrete and continuous variables. % These hybrid domains pose substantial problems: on one side, a continuous domain requires very expressive formal languages; on the other side, the resulting expressiveness results in highly intractable problems.

In this paper, we address the problem of requirements validation for real-world hybrid domains, and present two main contributions. % First, we propose the HRELTL logic, that extends the Linear-time Temporal Logic with Regular Expressions (RELTL) with hybrid aspects. % Second, we show that the satisfiability problem for the linear fragment can be reduced to an equi-satisfiable problem for RELTL. This makes it possible to use automatic (albeit incomplete) techniques based on Bounded Model Checking and on Satisfiability Modulo Theory.

The choice of the language is inspired by and validated within a project funded by the European Railway Agency, on the formalization and validation of the European Train Control System specifications. The activity showed that most of requirements can be formalized into HRELTL, and an experimental evaluation confirmed the practicality of the analyses.

11:30 Hongyang Qu, Marta Kwiatkowska, Gethin Norman and David Parker
Assume-Guarantee Verification for Probabilistic Systems

We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to verification, where both the assumptions made about system components and the guarantees that they provide are regular safety properties, represented by finite automata. Unlike previous proposals for assume-guarantee reasoning about probabilistic systems, our approach does not require that components interact in a fully synchronous fashion. In addition, the compositional verification method is efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. We present asymmetric and circular assume-guarantee rules, and show how they can be adapted to form quantitative queries, yielding lower and upper bounds on the actual probabilities that a property is satisfied. Our techniques have been implemented and applied to several large case studies, including instances where conventional probabilistic verification is infeasible.

12:00 Will Harwood, John Clark and Jeremy Jacob
Boolean Coherence: Does it make sense?

We continually face the problem of making sense of the world by resolving conflicting reports from multiple sources of information. This is particularly so if we attempt to formulate Qualitative Safety Arguments. Traditional logic offers little to assist in this process.

In every day reasoning we usually assume that, without information to the contrary, we should use all information from all sources and that "information to the contrary" is the presence of an inconsistency between the sources. In order to resolve these conflicts we must make use of additional information which gives preference to one source of information over another when conflict arises between sources.

The suggestion put forward in this note is that it is possible to reach a "best'" conclusion by taking the most coherent theory that respects the preference ordering on sources and that this theory is the maximal consistent theory with respect to the ordering. This process is parameterized by an underlying notion of logic that provides the notions of consistency and entailment. This notion is straightforward when applied to the standard notion of a strict preference ordering but is a little more involved when we consider partially ordered preferences.

14:00‑15:00 Invited Talk
Location: AT 2.12
14:00 César A. Muñoz (NASA Langley)
A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems

In order to accommodate the predicted increase in air traffic operations over the next decades, the next generation of air transportation systems rely on new operational concepts where the responsibility for traffic separation is air/ground distributed. These new concepts will require an unprecedented level of safety-critical systems. State-based distributed Separation Assurance (SA) is one of such concepts and it refers to conflict prevention, detection, and resolution systems that rely exclusively on the state information, i.e., 3-D position and velocity vectors, that is broadcast by each aircraft.

This talk presents the Airborne Coordinated Conflict Resolution and Detection (ACCoRD) framework for the design and verification of state-based separation assurance systems. The framework, which has been specified and mechanically verified in PVS, consists of a set of definitions and formally proven criteria that guarantee the correctness of a family of SA algorithms. For instance, in the case of pairwise conflict resolution, ACCoRD provides criteria that guarantee that two distributed algorithms, which satisfy the same coordination criteria, independently compute resolution maneuvers that yield conflict free trajectories when simultaneously implemented by the aircraft. This talk gives more examples of such criteria and algorithms that satisfy them. It also argues that a criteria-based verification framework, such as ACCoRD, will enable the natural evolution of the worldwide Air Transportation System.

15:30‑17:15 Session 2
Location: AT 2.12
15:30 Yun Zhu, Edwin Westbrook, Jun Inoue, Alexandre Chapoutot, Cherif Salama, Marisa Peralta, Travis Martin, walid taha, Marcia O'Malley, Robert Cartwright, Aaron Ames and Raktim Bhattacharya
Mathematical Equations as Executable Models of Mechanical Systems

Domain-specific languages (DSLs) are a key tool for productivity. This is because they allow users to write programs for a specific in a manner that is natural for that domain, allowing such programs to be written quickly and easily. In this paper (presented at ICCPS '10), we have analyzed what components are needed in a DSL to help mechanical engineers model cyber-physical systems, and we have investigated how to define the semantics of such a DSL. We have designed a DSL, called Acumen, which allows mechanical engineers to specify cyber-physical systems using a rich language of differential equations for the physical components, including families of equations, partial derivatives, and recursive functions. These components are all necessary for current engineering practice. Discrete components are specified with a simple event-driven programming language. Acumen then compiles the specifications for physical components into explicit ODEs, which, along with the event-driven programs, can then be simulated using standard tools.

In this talk, we will focus on the next step of cyber-physical design, namely, verification. Techniques have been developed for the compilation target of Acumen, i.e., explicit ODEs with simple discrete programs. None of these techniques, however, have considered a rich set of features like that of Acumen's language for specifying physical systems. We present this as a challenge to the verification community: how do we verify properties of programs in a language like Acumen? Can existing techniques for the target language be modified to work for the source language? Can automated techniques be used, or will cyber-physical system designers need to write some proofs manually? If manual proofs are needed, what sort of proof language would make this task easiest for engineers?

16:00 Stefan Ratschan
Interval Constraint Propagation as a Tool for Deductions about Mixed Discrete/Continuous Systems

Interval Constraint Propagation is used as the underlying technique for several tools for verifying hybrid systems. In the talk, we will present interval constraint propagation as a general algorithmic tool for deductions about mixed discrete/continuous systems. We will discuss its advantages and limitations for its usage with such systems, and an outlook on how these limitations might be overcome. Moreover, we will discuss the specific usage of interval constraint propagation in our tool HSolver.

16:30 Grant Olney Passmore and Paul B. Jackson
Introductory Tutorial: Combined Decision Techniques for the Existential Theory of the Reals
16:45 Florent Kirchner and Grant Olney Passmore
Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations

RAHD [4] is a tool that takes advantage of a heterogeneous collection of proof procedures to decide the satisfiability of formulas in the existential fragment of the theory of real closed fields. But system analysts can rarely restrict themselves only to arithmetic-based problems: they might want to use RAHD as part of a more diverse formal toolbox. In this paper, we present ongoing work on an architecture that enables the skeptical integration of RAHD into general-purpose proof assistants (PA). We will present a system-level view of how this integration can be performed, and examine a major concern of this implementation: efficiency. The latter is addressed by using a number of techniques, from the use of a minimalistic proof description language to the introduction of a novel staged refinement procedure to the recourse to carefully chosen and optimized data-structures [2]. While we are especially interested in the Coq PA, where RAHD can supplement a burgeoning collection of arithmetic tactics [3,1,5], we envision other tools such as Isabelle, HOL, or PVS taking advantage of this development.