The 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’16) will take place April 11, 2016 in Vienna, Austria as a satellite event of CPSWeek 2016.
Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems.
There are several successful methods for hybrid systems reachability analysis. Some methods explicitly construct flow-pipes that overapproximate the set of reachable states over time, where efficient computation of such overapproximations requires symbolic representations such as support functions. Other methods based on satisfiability checking technologies, symbolically encode reachability properties as logical formulas, while solving such formulas requires numerically-driven decision procedures. Last but not least, also automated deduction and the usage of theorem provers led to efficient analysis approaches. The goal of this workshop is to bring together researchers working with different reachability analysis techniques and to seek for synergies between symbolic and numerical approaches.
The SNR workshop solicits papers broadly in the area of verification and synthesis of continuous and hybrid systems. The scope of the workshop includes, but is not restricted to, the following topics:
- Reachability analysis approaches for hybrid systems
- Flow-pipe construction; symbolic state set representations
- Trajectory generation from symbolic paths; counterexample computation
- Abstraction techniques for hybrid systems
- Reliable integration
- Decision procedures for real arithmetic
- Automated deduction
- Logics to reason about hybrid systems
- Reachability analysis for planning and synthesis
- Domain-specific approaches in biology, robotics, etc.
- Stochastic/probabilistic hybrid systems
The workshop solicits long papers (maximal 10 pages) and short papers (maximal 6 pages). Submissions must present original unpublished work which is not submitted elsewhere. They should be written in English and formatted according to the IEEE guidelines for conference proceedings.
Papers can be submitted using the EasyChair system.
All submissions will undergo a peer-reviewing process. Accepted papers will be published electronically in the IEEE Xplore Digital Library.
The call for papers (ASCII) can be downloaded here.
|Author notification||March 9, 2016|
|Workshop||April 11, 2016|
Przemysław Daca (Institute of Science and Technology Austria, Austria)
Matthias Althoff (Technische Universität München, Germany)
Ezio Bartocci (Vienna University of Technology, Austria)
Parasara Sridhar Duggirala (University of Connecticut, USA)
Martin Fränzle (University of Oldenburg, Germany)
Goran Frehse (Verimag, France)
Sicun Gao (MIT, USA)
Antoine Girard (L2S, CNRS, France)
Taylor T. Johnson (University of Texas at Arlington, USA)
Mircea Lazar (Technische Universiteit Eindhoven, The Netherlands)
Maria Prandini (Politecnico di Milano, Italy)
Stefan Ratschan (Academy of Sciences, Czech Republic)
Rajarshi Ray (National Institute of Technology Meghalaya, India)
Sriram Sankaranarayanan (University of Colorado Boulder, USA)
Ashish Tiwari (SRI, USA)
Stavros Tripakis (Aalto University, Finland, and UC Berkeley, USA)
Martin Wehrle (University of Basel, Switzerland)
Edmund Widl (Austrian Institute of Technology, Austria)
Paolo Zuliani (University of Newcastle, UK)
Stylianos Basagiannis (United Technologies Research Center, Ireland)
Formal Verification towards Software Safety-Critical Certification of Airborne Systems under DO-178C
Airborne systems are considered to compose a highly complex network of interconnected Cyber-Physical Systems (CPS). Following the ARP-4754A development guidelines, a series of multidisciplinary engineers have to decompose system, hardware and software requirements in order to validate their correctness. In the same line, requirements traceability, validation and verification is considered to be a crucial part of certification processes for both hardware (DO-254) and software (DO-178C) components. System intrinsic complexity though, imposed by CPS(s), constitutes the certification of airborne systems a difficult, time-consuming and often expensive task. In this paper we review challenges and solutions for software certification under the DO-178C standard using formal verification in line with new CPS analysis evolution. We describe current model-based design methodologies followed today in the aerospace domain and comment on new tool-aided work-flows and techniques that could accelerate the software certification processes with respect to CPS(s) requirements.
Thao Dang (Verimag, France)
Template Complex Zonotopes: A New Set Representation for Verification of Hybrid Systems
In this work, we propose a new set representation, called template complex zonotope, which extends the usual definition of zonotopes to the complex domain. Indeed, the generators of a complex zonotope are complex-valued vectors and each coefficient in their linear combinations is bounded in absolute value. The term “template” refers to the fact that the generators are fixed a priori. Geometrically speaking, a template complex zonotope is the Minkowski sum of line segments and ellipsoids, which allows this representation to describe, in addition to usual zonotopes, non-polyhedral convex sets. Other extensions of zonotopes, such as quadratic [Adje2015] and more generally polynomial zonotopes [Althoff201] have been proposed. However, template complex zonotopes introduced in our paper are different from polynomial zonotopes as follows. A polynomial zonotope is a set-valued polynomial function of intervals, whereas a template complex zonotope is a set valued function of circles in the complex plane. As we shall show in the paper, the main advantage of this set representation is that we can exploit the eigenstructures of a linear system to define good templates for good convergence of fixed point computations, arising in reachability analysis as well as invariant computation. Indeed, template complex zonotopes can efficiently capture positive invariants of a linear system (without switching) by having the eigenvectors of the corresponding matrix as generators. Motivated by this, we consider applications to discrete-time switched linear systems with additive disturbances and nearly periodic linear impulsive systems, two important classes of hybrid models which widely used for design and implementation of embedded control systems (see for example [blanchini2015, Naghshtabrizi2007,Naghshtabrizi2008] and references there in). The presentation is organized as follows. We first describe template complex zonotopes and the computation of some important operations required by verification procedures. We then show how this new set representation can be used to verify linear invariance properties of linear switched systems with additive disturbance. In the next section, we present another application to verification of stability of linear impulsive systems. Finally to demonstrate the efficiency of template complex zonotopes, we provide experimental results which are either better or competitive compared to the existing results.
These results were obtained in collaboration with Arvind S. Adimoolam (VERIMAG).
Walid Taha (Halmstad University, Sweden)
Accurate Rigorous Simulation Should be Possible for Good Designs
The development of Cyber-Physical Systems benefits from better methods and tools to support the simulation and verification of hybrid (continuous/discrete) models. Acumen is an open source testbed for exploring the design space of what rigorous-but-practical next-generation tools can deliver to developers. Central to Acumen is the notion of rigorous simulation. Like verification tools, rigorous simulation is intended to provide guarantees about the behavior of the system. Like traditional simulation tools, it is intended to be intuitive, practical, and scalable. Whether these two goals can be achieved simultaneously is an important, long-term challenge.
This paper proposes a design principle that can play an important role in meeting this challenge. The principle addresses
the criticism that accumulating numerical errors is a serious impediment to practical rigorous simulation. It is inspired by a twofold insight: one relating to the nature of systems engineered in the real world, and the other relating to how numerical errors in the simulation of a model can be recast as errors in the state or parameters of the model in the simulation. We present a suite of small, concrete benchmarks that can be used to assess the extent to which a rigorous simulator upholds the proposed principle. We also report on which benchmarks Acumen’s current rigorous simulator already succeeds and which ones remain challenging.
9:00-10:30 Session 1: Validated simulation (Session chair: Andrew Sogokon)
9:00-10:00 Invited talk
Adam Duracz, Ferenc Bartha and Walid Taha.
Accurate Rigorous Simulation Should be Possible for Good Designs
Adrien Le Coent, Julien Alexandre Dit Sandretto, Alexandre Chapoutot and Laurent Fribourg.
Control of Nonlinear Switched Systems Based on Validated Simulation
11:00-12:30 Session 2: Formal methods in industry (Session chairs: Erika Abraham, Sergiy Bogomolov)
11:00-12:00 Invited talk
Software Certification of Airborne Cyber-Physical Systems under DO-178C
12:00-12:30 Podium discussion
Formal Methods: Bridging the Gap Between Academic and Industrial Research
14:00-15:30 Session 3: Reachability analysis (Session chair: Maria Prandini)
14:00-15:00 Invited talk
Santosh Arvind Adimoolam and Thao Dang.
Template complex zonotopes: A new set representation for verification of hybrid systems
Computing ODE-barriers in Hyper-rectangles
16:00-17:30 Session 4: Discrete-time and probabilistic systems (Session chair: Parasara Sridhar Duggirala)
Riccardo Vignali and Maria Prandini.
Model reduction of discrete time hybrid systems: A structural approach based on observability
Yang Gao and Martin Fränzle.
CSiSAT: A Satisfiability Solver for SMT Formulas with Continuous Probability Distributions
Kristóf Marussy, Attila Klenik, Vince Molnár, András Vörös, Miklós Telek and István Majzik.
Configurable Numerical Analysis for Stochastic Systems