Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2017 | Book

Verification of Networks of Smart Energy Systems over the Cloud Read chapter Read first chapter

Numerical Software Verification

9th International Workshop, NSV 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers

Editors: Sergiy Bogomolov, Matthieu Martel, Pavithra Prabhakar

Publisher: Springer International Publishing

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

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.

Table of Contents

Frontmatter
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.
Assalé Adjé
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.
Behzad Samadi
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.
Yassamine Seladji
Backmatter
Metadata
Title
Numerical Software Verification
Editors
Sergiy Bogomolov
Matthieu Martel
Pavithra Prabhakar
Copyright Year
2017
Electronic ISBN
978-3-319-54292-8
Print ISBN
978-3-319-54291-1
DOI
https://doi.org/10.1007/978-3-319-54292-8

Premium Partner

    Image Credits