Rigorous High Order Computation with Taylor Models and Its Applications

Speaker: Martin Berz (Michigan State University, USA).

Abstract:

The rigorous control of algorithmic errors, model inaccuracies, and limitations due to floating point accuracies is a fundamental necessity for the safe and dependable operation of engineering systems. Recent advances in the field of rigorous computing have focused on the development of tools that allows the represenation of computational quantities with a fully verified error that scales with a high order of the domain size. Compared to conventional interval methods, the resulting Taylor Model methods lead to significantly more favorable accuracies when studying larger domains.

The methods lend themselves well for the application to standard problems of verified computation, including the rigorous solutions of flows of ODEs, rigorous global optimization, and constraint satisfaction. The core algorithmic ideas of these approaches will be reviewed.

Finally, we present a number of practical applications of the new techniques from various fields of Science and Engineering, including simulation and analysis of large particle accelerators, study of the dynamics and possible impact of near-earth asteroids, and applications in computer assisted proofs about hyperbolic and chaotic dynamics.

Formal methods in computerized control design, a tentative overview

Speaker: Paul Caspi (Vermiag, France).

Abstract:

In this presentation we first remark that computerised control applies to many safety-critical systems and is thus one of the fields where formal methods should be used with higher priority. But we also remark that most of theses systems are developed without applying many, if any formal methods, The situation is slowly changing and for instance, abstract interpretation is gaining confidence in execution error and timing analysis. Yet, as far as functional design is concerned, the state of art is less positive and we try to analyse why. Several reasons are reviewed: the different point of views of computer science and control theory on formal development and the hybrid aspect of complex control applications. We conclude by reviewing some recent efforts addressing these issues.

Formal Verification of Avionics Software in a Model-Based Development Process

Speaker: Michael Whalen (Rockwell Collins, USA).

Abstract:

The next generation of military aerospace systems will include advanced control systems whose size and complexity will challenge current verification and validation approaches. The recent adoption by the aerospace industry of model-based development tools such as SimulinkR and SCADE SuiteT facilitates the use of formal methods for the verification of critical avionics software. Formal methods use mathematics to prove that software design models meet their requirements, and so can greatly increase confidence in the safety and correctness of software. Recent advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle.

Verification of numeric software with non-linear operations is an extremely challenging problem. Most model checkers do not have any native support for non-linear arithmetic over real numbers. Even with such support, results are not necessarily sound with respect to floating-point implementations. Exact representations of floating point numbers and operations are complex and difficult to scale beyond single-operation models. On the other hand, it is possible to use approximations to check interesting properties of large, numerically-intensive software. In this talk, we describe a handful of mechanisms for abstraction and composition that have been used at Rockwell Collins, Inc. to reason about numeric software, and some results from applying the techniques to industrial control systems. Using these techniques, we have found subtle errors in Simulink controller models involving over 2000 basic blocks.

Trajectory based analysis of cyber-physical systems using approximate bisimulation.

Speaker: A. Agung Julius (RPI, USA)

Abstract:

In this talk I will present the applications of approximate bisimulation in trajectory based analysis of CPS. In particular, I will review earlier work (by several authors) on trajectory based safety analysis for deterministic and stochastic systems. This exposition will be followed by some discussion on further application in event timing analysis and verification of properties expressed as temporal logic formulae.

Formally Analyzing Adaptive Flight Control

Speaker: Ashish Tiwari (SRI, USA)

Abstract:

We formally verify a direct model-reference adaptive control (MRAC) method that is used to enable flight control in adverse conditions. We use the "bounded verification" approach and verify the system by introducing templates for both the assumptions and the guarantees. We use the tool QEPCAD to solve the resulting formula that contains both existential and universal quantifiers.

Control of Hybrid Automata with Imperfect Mode Information Assuming Separation between Estimation and Control

Speaker: Domitilla Del Vecchio (University of Michigan)

Abstract:

The safety control problem for hybrid automata with imperfect mode information and continuous control is addressed. When the controller does not have access to the mode of the system, available static feedback techniques for safety control cannot be applied. We thus propose a dynamic feedback strategy in which a mode estimator is run to construct the set of possible current system modes compatible with the dynamics of the system and with the measurements. A control map is then constructed that, on the basis of the current mode estimates, returns the set of all possible safe control inputs. This dynamic feedback structure implicitly assumes separation between state estimation and control design. The obtained dynamic feedback maintains safety by design and is the least restrictive given the chosen mode estimator. Termination conditions for the algorithms that compute the dynamic feedback map are provided. Furthermore, for the class of order preserving hybrid automata, we show that the algorithm that computes the control map has linear complexity with the number of continuous variables. The proposed control technique is applied to a semi-autonomous cooperative active safety system, which belongs to the class of order preserving hybrid automata.

Using Box Splines to Approximate Reachable Sets of Polynomial Systems

Speaker: Thao Dang (Verimag, France)

Abstract:

In this paper we describe a method for over-approximating the reachable sets of dynamical systems described by polynomial differential or difference equations. This problem arises in many safety verification problems for systems originating from biological and chemical engineering applications. These equations can also arise in the control software which implements some numerical discretization of an embedded controller. This method is based on the box spline representation of polynomials, the coefficients of which can be used to enclose all the reachable points. Compared to our previous method using the Bezier simplex representation, this method deals with rectangular domains, which are simpler to handle than simplices.

Range Estimation of Floating-Point Variables in Simulink Models

Speaker: Alexandre Chapoutot (LIP6 - PEQUAN)

Abstract:

The transformation of floating-point programs into fixed-point equivalent programs is a challenge because the behaviors of these arithmetics are different. Generally, this transformation is facilitated thanks to a two steps analysis of the design. The first step consists in inferring the range of values for each variables. The second step is the analysis of the precision of the computations taking into account the rounding-errors. In our talk, we will present a new statistical method for inferring dynamic range of floating-point variables in Simulink models. Our approach is based on the extreme value theory. Experimental results will also be presented.

Morphisms for Analysis of Hybrid Systems.

Speaker: Rachid Rebiha (Univ Lugano and IC Unicamp)

Abstract:

We present a new method for generating ideals of non-linear invariants of hybrid systems with algebraic differential and local rules (without using Grobner basis, quantifier elimination or cylindrical algebraic decomposition). We reduce the non-trivial invariants generation problem to linear algebra by encoding consecution requirements as specific morphisms represented by matrices. Our algorithm has a strategy for guessing optimal degree bounds and return a basis of an ideal of non-trivial non linear invariants.

Verification of Floating Point Computations Using Polyhedral Domains

Speaker: Goran Frehse (Verimag, France)

Abstract:

In model-based design, numerical code is automatically generated from high-level designs. Verification of numerical code is, therefore, an important problem in embedded systems, where model-based design is widely used. Code execution on a target processor can lead to overflow, underflow, error accumulation, divide by zero, etc., due to compiler optimizations and the processor representation of floating-point numbers. We present a methodology to compute bounds on the variables in numerical code with linear arithmetic that takes these effects into account. Our approach is based on a static analysis technique for polyhedral domains. We introduce a new widening operator that performs better than standard widening on numerical code. We also present heuristics for reducing the complexity of the analysis. These techniques have been implemented using PHAVer, a linear hybrid automata reachability analysis tool. We compare our approach with existing techniques on some examples.
Last modified: Wed Jul 16 08:38:31 EDT 2008