AbSynth 2015

Abstraction and Synthesis of Correct-by-Construction Robotics Software: Reuniting Formal Methods with Model-Driven Software Engineering.

Invited Speakers



  • Prof. Calin Belta, Boston University, USA
  • Title: Formal Synthesis of Control Strategies for Dynamical Systems

    Abstract: Calin Belta In control theory, complex models of physical processes, such as systems of differential equations, are usually checked against simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as languages and formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition graphs. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinite-space continuous and hybrid systems. However, provably correct but conservative approaches, in which the satisfaction of a property by a dynamical system is implied by the satisfaction of the property by a finite over-approximation (abstraction) of the system, have received a lot of attention in recent years. The focus of this talk is on synthesis. It is first shown that game-based control strategies for finite systems can be adapted to produce conservative approaches to control of continuous-time and discrete-time dynamical systems. It is then shown then refinement and Lyapunov-based techniques can be used to reduce the conservatism. The usefulness of these computational tools is illustrated with various examples.

  • Prof. Davide Brugali, University of Bergamo, Italy
  • Title: Model-Driven Engineering for Robotic Software Product Lines

    Abstract: Davide Brugali The cost of creating new robotics products is significantly related to the complexity of developing software control systems that are flexible enough to easily accommodate frequently changing requirements: more advanced tasks in highly dynamic environments, in collaboration with unskilled users, and in compliance with changing regulations. In various application domains software product line (SPL) development has proven to be the most effective approach to face this kind of challenges. A SPL is a set of software intensive systems that share a common set of features for satisfying a particular market segment's needs. Each new application is built from the SPL repository of common software assets (e.g. architectural models, software components). Typically, a SPL is a strategic investment for organizations, which wants to achieve customer value through large commercial diversity of their proucts with a minimum of technical diversity at minimal cost. The talk will illustrate our experience in developing MDE tools for modeling and configuring robotic SPL.

  • Prof. Alessandro Abate, University of Oxford, UK
  • Title: Data-driven and model-based quantitative verification and correct-by-design synthesis

    Abstract: Alessandro Abate I discuss a new and formal, measurement-driven and model-based automated verification and synthesis technique, to be applied on quantitative properties over systems with partly unknown dynamics. I explicitly focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a model-based verification procedure. While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on systems represented via stochastic hybrid models, which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear). With focus on the model-based verification procedure, I provide the characterisation of general temporal specifications based on Bellman's dynamics programming. The computation of such properties and the synthesis of related control architectures optimising the properties of interest is attained via the development of abstraction techniques based on quantitative approximations. This abstraction approach employs techniques and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control.

  • Prof. Erika Abraham, RWTH Aachen University, Germany
  • Title: A Greedy Approach for the Efficient Repair of Stochastic Controller Models

    Abstract: Erika Abraham Probabilistic modelling languages are popular formalisms to model systems with randomized components in their behaviour. Probabilistic models play an important role also in robotics, for example when modelling controllers. A great advantage of formal models is that they allow the application of formal methods for their analysis. For discrete-time probabilistic models there are efficient methods to check whether they satisfy certain properties. If a property is refuted, available techniques can be used to explain the failure in form of a counterexample. However, there are no scalable approaches to repair a model, i.e., to modify it with respect to certain side conditions such that the property is satisfied. In this talk we discuss such a method, which avoids expensive computations and is therefore applicable to large models.

  • Prof. Herman Bruyninckx, KU Leuven and Eindhoven University of Technology
  • Title: Model-Driven Engineering for Knowledge Representation and formal software modelling and interfacing

    Abstract: Felix Ingrand Model-Driven Engineering has often been limited to the OMG's "Model-Driven Architecture" version of the concept, which is far more limited than what robotics needs. In an only somewhat more extensive interpretation of the term "MDE", the approach lends itself very well to formal representation of knowledge relationships. This talk explains our current research that gives such a KR interpretation to MDE, using new JSON-based formal languages (JSON-schema and JSON-LD), to model software modules and interfaces. The approach can circumvent the difficult problem of having "to ground" models into code by code generation, by replacing it with query-based interfaces between robot "task" modules and "platform" modules. Concrete examples are given of formal models for "bottom up" representations of robot motion capabilities, starting with (finally....) a concrete formal standard for the representation of frames and closely related geometric concepts that play a fundamental role in robotics.

  • Prof. Rudiger Ehlers, University of Bremen, Germany
  • Title: How can reactive synthesis help with model-based design of robot control strategies?

    Abstract: Ruediger Ehlers Designing robot control software is difficult on many levels: not only do engineers have to cope with the intricacies of the robot's physical workspace, but they also have to coordinate the robot's many tasks in an efficient and effective way. Model-based design helps with tackling both problems by allowing the evaluation of a controller design before it is fully implemented. However, most evaluation and testing techniques can only be applied once a model is complete enough to be executable, and hence after considerable effort has been spent on the design. This leads to a high cost of changes to the design that may be needed because the design is later found to have an insufficient performance or because of requirement changes. This talk presents a multitude of ways in which reactive synthesis can help to work with incomplete models of the system and its environment. We show how the system's specification can be debugged by analyzing the properties that all implementations to a specification must have. Apart from analyzing in which cases a controller is bound to fail, we show how to analyze how error-resilient a robot controller implementation can be and how to compute the achievable resource consumption rates (time/energy/robot travel distance) of the controller before it has been constructed. The methods presented thus help with the engineering process by giving early feedback and help to mediate between user expectations and the system design.

  • Prof. Goran Frehse, Universite Joseph Fourier, France
  • Title: Reachability Analysis of Piecewise Affine Systems Using Support Functions

    Abstract: Goran Frehse In model-based design, a mathematical model of a plant is used to construct a controller that achieves a certain performance (e.g., rise or settling time) while satisfying certain critical "safety" constraints (e.g., saturation, overflow). It can be hard to verify that performance and safety requirements are met, in particular when the controlled system has complex dynamics (mode switching) or when the operating conditions are uncertain (varying initial conditions, disturbances, parameter variations). Techniques such as Monte-Carlo and corner case simulation help to gain confidence in the design, but require a large number of simulation runs and generally do not provide conservative answers. Symbolic simulation, also referred to as reachability analysis, can complement such trajectory-based analysis techniques. Instead of computing a sequence of points on a single trajectory, we compute a sequence of sets that covers all possible trajectories of the system. Computing with sets allows us to use conservative over-approximations and take into account various kinds of nondeterminism in the plant and the controller. While computing with sets is inherently costly and has long been restricted to toy problems, recent advances based on implicit ("lazy") set representations have made symbolic simulation applicable to linear ODEs with hundreds of variables. In this talk, we present the symbolic simulation algorithm of our verification platform SpaceEx. We illustrate its performance with examples from various application domains and highlight some of the mathematical tricks that make this approach both precise and scalable.

  • Prof. Felix Ingrand, LAAS, France
  • Title: Validating and verifying robot functional components

    Abstract: Felix Ingrand Most robotics systems use some framework to deploy the functional components in charge of sensors (camera, laser range finder, etc), effectors (wheels, pan and tilt unit, arms, etc), as well as data processing (stereo correlation, map building, SLAM, motion planning, etc). We consider that this set of components constitute the functional layer of the robot. The decisional layer, in charge of planning, acting, monitoring, etc usually uses other types of framework. If one considers validating and verifying formal properties on these different software, the decisional components are often model based, which model can often be checked and verified. As for the functional components, most development frameworks and middleware do not consider validation and verification, despite the increasing need to robustify and certify robotics systems (e.g., autonomous cars, service robots, coworker robots).

    For the last 30 years, the LAAS robotic group has been using the GenoM framework to develop the functional components on its various robots. A GenoM module is specified with: tasks (periodic or aperiodic); services which are associated to tasks; and ports (which allow modules to share data between each others). Each service is specified with an automata, with each state calling a particular elementary C or C++ code (codel), whose returned value when executing specifies the next state. Temporal information are specified for periodic tasks (period) and also for codels (WCET).

    The latest version of GenoM (GenoM3) is template based, and from a particular GenoM specification can generate a number of programs or libraries: 1) the module itself for different middleware (e.g. Pocolibs, ROS-Com, Orocos), linked with the associated codels library, 2)client libraries (e.g. c-client, OpenPRS client, TCL client)

    We are also using this template mechanism to also produce formal models of the functional modules. We have identified two formal frameworks for which we can automatically synthesize a model. Fiacre/TINA is a framework developed at LAAS/VerTICS to model time constrained distributed/concurrent systems. The underlying formalism is Fiacre, a high level notation targeting Time Petri nets enriched with priorities and data processing. One can verify expected properties, with model checking, expressed in temporal logics (LTL) or Fiacre property language (realtime property patterns). Such properties can be checked over one particular modules or better over a set of concurrently executing modules.


  • Prof. Joost-Pieter Katoen, RWTH Aachen University, Germany
  • Title: Efficient Parameter Synthesis in Probabilistic Models

    Abstract: J-P Katoen We present several techniques for analyzing parametric Markov chains (pMCs), chains in which the transitions are labeled with polynomials over in the set of model variables. The core is to compute a rational function (i.e., a fraction of two polynomials in the model parameters) for reachability and expected reward objectives. Our technique outperforms state-of-the-art tools and supports computing conditional probabilities over pMCs. This is supplemented by support for incremental automatic parameter synthesis (using SMT techniques) to determine "safe" and "unsafe" regions of the parameter space. All values in these regions give rise to instantiated MCs satisfying or violating the (conditional) probability or expected reward objective. Experimental results show that our techniques scale to MCs with millions of states and several parameters. The techniques are supported by the web-based PROPhESY tool supporting visualization and user-guided parameter synthesis.

  • Prof. Hadas Kress-Gazit, Cornell University, USA
  • Title: Synthesis for robots: they either behave well or explain why they can't

    Abstract: Jun Liu The traditional paradigm of programming a robot is to write code and test; this approach is time consuming, error prone and even worse, if the robot behaves as expected during testing, it does not mean that it will behave well, or as expected, in the future. In the past few years, reactive synthesis has been used to generate correct-by-construction robot controllers that provide guarantees for robot behaviors if synthesis succeeds, and provide explanations for why the robot may fail when synthesis fails. In this talk I will focus on how the robot can explain failure cases - when the robot cannot guarantee it can do what is expected due to problems in its specifications, its environment or its dynamics - and what suggestions it can autonomously give to fix the problems.

  • Prof. Jun Liu, University of Sheffield, UK
  • Title: Finite Abstractions for Robust Synthesis

    Abstract: Jun Liu Construction of finite abstractions for nonlinear systems is a critical step when applying abstraction-based formal approaches to hybrid control synthesis. Such approaches have gained popularity in recent years for their ability to handle control synthesis problems for complex dynamical systems with high-level, rigorous specifications. In practice, dynamical systems are often affected by imperfections, such as measurement errors, delays, and disturbances. Synthesis of robust control strategies thus becomes important. In this talk, I will present a notion of finite abstractions that can be used for robust control synthesis. I will focus on nonlinear dynamical systems described by differential equations, with specifications expressible in linear temporal logics. I will present computationally efficient procedures for abstracting nonlinear dynamics into finite-state transitions and discuss how analytical tools from dynamical system theory can provide correctness and robustness guarantees for these abstractions. Connections with reachability analysis will also be discussed, where I will focus on how computation of better over-approximations of local reachable sets can lead to less conservative abstractions. The results will be illustrated with several applications in robot motion planning and automotive adaptive cruise control.