main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 9th InternationalWorkshop on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July 2011 - colocated with CAV 2016, the 28th International Conference on Computer Aided Verification.

The NSV workshop is dedicated to the development of logical and mathematical techniques for the reasoning about programmability and reliability.

Inhaltsverzeichnis

Verification of Networks of Smart Energy Systems over the Cloud

Abstract
This contribution advocates the use of formal methods to verify and certifiably control the behaviour of computational devices interacting over a shared infrastructure. Formal techniques can provide compelling solutions not only when safety-critical goals are the target, but also to tackle verification and synthesis problems on populations of such devices: we argue that alternative solutions based on classical analytical techniques or on approximate computations are prone to errors with global repercussions, and instead propose an approach based on formal abstractions, error-based refinements, and the use of interface functions for the synthesis of abstract controllers and their concrete implementation. Two applicative areas are elucidated, dealing respectively with thermal loads and electricity-generating devices interacting over a smart energy network or over a local power grid. We discuss the aggregation of large populations of thermostatically-controlled loads and of photovoltaic panels, and the corresponding problems of energy management in smart buildings, of demand-response on smart grids, and respectively of frequency stabilisation and grid robustness.
Alessandro Abate

Proving Properties on PWA Systems Using Copositive and Semidefinite Programming

Abstract
In this paper, we present a model based on copositive programming and semidefinite relaxations of it to prove properties on discrete-time piecewise affine systems. We consider invariant i.e. properties represented by a set and formulated as all reachable values are included in the set. Also, we restrict the analysis to sublevel sets of quadratic forms i.e. ellipsoids. In this case, to check the property is equivalent to solve a quadratic maximization problem under the constraint that the decision variable belongs to the reachable values set. This maximization problem is relaxed using an abstraction of reachable values set by a union of truncated ellipsoids.

Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory

Abstract
Signal-flow-graph theory provides an efficient framework to model various engineering and physical systems at a higher-level of abstraction. In this paper, we present the formalization of the signal-flow-graph theory with an ultimate goal to conduct the formal analysis of engineering systems within a higher-order-logic theorem prover. In particular, our formalization can tackle system models which are based on undirected graphs. We also present the formalization of the system transfer function and associated properties such as stability and resonance. In order to demonstrate the effectiveness of our work, we present the formal analysis of two engineering systems namely the PANDA Vernier resonator and the z-source impedance network, which are commonly used in photonics and power electronics, respectively.
Sidi Mohamed Beillahi, Umair Siddique, Sofiène Tahar

Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest

Abstract
When a floating-point computation is done, it is most of the time incorrect. The rounding error can be bounded by folklore formulas, such as $$\varepsilon |x|$$ or $$\varepsilon |{\circ }(x)|$$. This gets more complicated when underflow is taken into account as an absolute term must be considered. Now, let us compute this error bound in practice. A common method is to use a directed rounding in order to be sure to get an over-approximation of this error bound. This article describes an algorithm that computes a correct bound using only rounding to nearest, therefore without requiring a costly change of the rounding mode. This is formally proved using the Coq formal proof assistant to increase the trust in this algorithm.
Sylvie Boldo

Studying Sequences of Jumps in Hybrid Systems to Detect Zeno Phenomenon

Abstract
We propose a numerical analysis of sequences of points of interest associated to the dynamics of hybrid systems. These sequences are made of instants of switching mode or instants when a particular quantity vanishes. This analysis allows one to discover instant of accumulation points, a.k.a. Zeno phenomenon. Some examples are given to show the potential of this approach.
Alexandre Chapoutot, Julien Alexandre dit Sandretto

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis

Abstract
We introduce FPBench, a standard benchmark format for validation and optimization of numerical accuracy in floating-point computations. FPBench is a first step toward addressing an increasing need in our community for comparisons and combinations of tools from different application domains. To this end, FPBench provides a basic floating-point benchmark format and accuracy measures for comparing different tools. The FPBench format and measures allow comparing and composing different floating-point tools. We describe the FPBench format and measures and show that FPBench expresses benchmarks from recent papers in the literature, by building an initial benchmark suite drawn from these papers. We intend for FPBench to grow into a standard benchmark suite for the members of the floating-point tools research community.
Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock

Falsification of Dynamical Systems – An Industrial Perspective

Abstract
Whenever formal verification of dynamical system models is not applicable, e.g., due to the presence of black-box components, simulation-based verification and falsification methods are promising approaches to gain confidence in a system satisfying its specification. With the introduction of robust semantics it is not only possible to answer this question in the Boolean sense but to quantify its truth. We illustrate a number of applications that are interesting from an industrial perspective, and point out how robustness could become even more versatile in the engineering process.
Thomas Heinz

Model Based Automatic Code Generation for Nonlinear Model Predictive Control

Abstract
This paper demonstrates a symbolic tool that generates C code for nonlinear model predictive controllers. The optimality conditions are derived in a quick tutorial on optimal control. A model based workflow using MapleSim for modeling and simulation, and Maple for analysis and code generation is then explained. In this paper, we assume to have a control model of a nonlinear plant in MapleSim. The first step of the workflow is to get the equations of the control model from MapleSim. These equations are usually in the form of differential algebraic equations. After converting the equations to ordinary differential equations, the C code for the model predictive controller is generated using a tool created in Maple. The resulting C code can be used to simulate the control algorithm and program the hardware controller. The proposed tool for automatic code generation for model predictive controllers is open and can be employed by users to create their own customized code generation tool.

Reduce the Complexity of the Polyhedron Minimization Using the Max Plus Pruning Method

Abstract
The polyhedral analysis is widely used for the static analysis of programs, thanks to its expressiveness but it is also time consuming. To deal with that, a sub-polyhedral analysis has been developed which offers a good tread off between expressiveness and sufficiency. This analysis is based on a set of directions which is defined statically at the beginning of the analysis. More the cardinality of $$\varDelta$$ is big, more the precision of the result is high. Even if the set $$\varDelta$$ is big, the sub-polyhedral analysis can be done in a linear time. The bottleneck is that to construct the resulting polyhedron with a large number of constraints (one constraints per direction) is time consuming. In this article, we present a minimization method that allows to deal with that, using the max plus pruning method. We demonstrate the efficiency of our method on some benchmarks. The first results are very encouraging.