Author Archives: Martin Fabian

Seminar – Simulation-based Techniques for Designing Reliable Cyber-Physical Systems

Wednesday 28 Feb at 13:15 in EL41

Alexandre Donzé

Cyber-Physical Systems (CPS) are computerized systems interacting with their physical environments. They are prominent in transportation (car, plane, rockets), robotics, internet of things, etc.  Control software for CPS has seen a dramatic increase in size and complexity in recent years. This is due to continuous pressure to optimize various aspects of the systems, such as, e.g., emissions and fuel efficiency in cars or more recently, the push toward more and more autonomous operations. The verification and validation of these software components are challenging because they are designed to influence and run in interaction with their physical environment. Ideally, testing necessitates a physical test-bed, a prototype, test tracks, etc. Such settings are costly and time-consuming, requiring hours in operating, collecting and analyzing data in order to get adequate confidence.  An additional layer of complexity arises from the fact that control software components are increasingly reliant on machine learning (ML) components. Contrary to component based on so-called “traditional” control theory, ML-based components provide very little guarantees of accuracy, stability or performance.

Decyphir develops simulation-based and monitoring approaches, implemented in the tool Breach, that provide some pragmatic solutions to these challenges. The tool revolves first around a principle of separation of concerns: what is a typical test case and how do we generalize it? Can we use a formal language to specify whether a test succeeded or not and how far it was from failing/succeeding? If these two relatively simple questions are answered, the main ‘trick’ of Breach is to compose the resulting test-case generator and monitor with various optimization strategies to find rare cases of failure (falsification), improve coverage, etc. Breach has been used to find bugs in complex industrial-size models, and more recently we looked into the problem of testing CPS in interaction with ML-based components, such as computer vision systems based on deep neural net (DNN). Much has been done and said about how to fool a DNN, and we do not claim deep contributions there but rather want to make the case that such analysis should be performed at, or at least in consideration of system-level requirements. We illustrate this point this with a toy example instrumented by Breach involving a simple driving game simulator and an automatic emergency braking system (AEBS) using a custom Python-based neural net trained to detect red cows on the road.

Alexandre Donzé – Biography

Alexandre Donzé is CTO and co-founder of Decyphir, Inc, building design automation tools for Cyber-Physical Systems. In 2007, he graduated from Grenoble University with a Ph.D in Computer Science and Mathematics on simulation-based verification of hybrid systems. In 2007-2008, He was a post-doctoral faculty at Carnegie Mellon University, working with Edmund M. Clarke and Bruce H. Krogh, where he contributed to the popularization of Statistical Model Checking, a highly scalable formal verification technique. From 2009 to 2012 as a researcher at Verimag Lab in Grenoble, he contributed to the development of SpaceEx, a leading reachability analysis tool for hybrid systems while conducting original research on Systems Biology. In March 2012, he joined the Department of Electrical Engineering and Computer Science of the University of California at Berkeley. A major focus of his research has been the development and use of Signal Temporal Logic (STL), a formal specification language used for model-based design of Cyber-physical systems (CPS), circuits, biological systems, etc. He is the author of Breach, a Matlab toolbox supporting various simulation-based techniques using STL specifications, which is getting a wide adoption in both academia and industry. He co-founded Decyphir, Inc. in November 2016.

Alexandre Donzé is visiting SyTeC as a guest researcher during February 26 to March 2.

Seminar – Designing controllers for hybrid systems using TuLiP

Seminar: Monday, February 19, 9.00-11.00 in EL43

Speaker: Ioannis Filippidis

TuLiP is a collection of tools for designing controllers for hybrid systems from specifications in temporal logic. The tools take as input a description of the system dynamics, a labeling of the geometry of interest, and the desired behavior as temporal logic formulas that describe assumptions about the environment and guarantees to be ensured by control design. Systems with piecewise affine dynamics and environmental disturbances are supported, together with discrete-valued variables that represent the system itself and its environment.

This presentation will describe the tools available in TuLiP, the Python user interface, as well as an overview of the algorithms for computing abstractions of continuous dynamics and synthesizing controllers at the discrete layer that implement the given assume-guarantee temporal logic specifications, subject to the constraints originating from the continuous dynamics.

Ioannis Filippidis – Decomposing formal specifications into assume-guarantee contracts for hierarchical system design

Seminar: 16 February 2018, 13:15, EL41

Speaker: Ioannis Filippidis, Caltech

The design of complex engineering systems is typically structured hierarchically by specifying individual subsystems, and their interaction. We describe a method to algorithmically decompose a given overall system specification into a contract of realizable component specifications that together implement the given specification. The decomposition algorithm
eliminates variables that are irrelevant to realizability of each component, in order to simplify the specifications and reduce the amount of information communicated between components. The variables to be eliminated are identified by parametrizing the information flow between components.

The specifications are written in the Temporal Logic of Actions, TLA+, with liveness properties restricted to a fragment known as GR(1). We study whether GR(1) contracts exist in the presence of full information, and prove that introducing either safety constraints or memory is necessary for decomposition, leading to a decomposition algorithm that avoids circularity. We formalize a definition of realizability in TLA+, and define an operator for forming open-systems from closed-systems, based on stepwise implication.

Our symbolic algorithms use binary decision diagrams (BDDs). To convert the generated specifications from BDDs to readable formulas, we symbolically solve a minimal covering problem. We implemented an algorithm for minimal covering over lattices originally proposed for two-level logic minimization. We formalized the computation of essential elements and cyclic core that is part of this algorithm, and machine-checked the proofs of safety properties using a proof assistant.

For presentation slides, please contact Dr Filippidis directly here.

Magic Tester – Automated testing in practice

SyTeC has now been part of introducing even more rigorous testing methods in industry. With collaboration in the research project TESTRON, the academically-developed MATLAB toolbox Breach is now being used at Volvo Car Corporation to automatically generate and run test vectors for hybrid and electric vehicle models at the Vehicle Propulsion department.

Above is a screenshot of the visualization tool provided for software testers, which easily gives access to statistics about the latest bugs found in the models, along with filtering options for any further information needed to fix the issues. The automatic tests run on a server around the clock and are done in early development phases to capture and fix bugs before these come even close to production code. Obviously, this significantly raises the confidence of the final implementations.

The accessibility of easy-to-understand visualization is paramount to spread more academic approaches to test engineers, which is why this development is considered great progress for TESTRON as well as SyTeC as a whole.

Ioannis Filippidis – Guest researcher visiting SyTeC

Dr. Ioannis Filippidis will be visiting Chalmers and specifically the SyTeC project as a guest researcher for three weeks from Feb 11, 2018, to March 2, 2018. During Dr. Filippidis’ visit, the primary focus will be on researching formal specification and automatic test case generation for hybrid systems.

Dr. Filippidis graduated in November 2017 with a Ph.D. in control and dynamical systems from the California Institute of Technology, where he investigated the automated decomposition of system specifications into contracts for interacting components. He holds a Diploma in Mechanical Engineering from the National Technical University of Athens, with a thesis on robot motion planning using navigation functions.

As an intern at the Jet Propulsion Laboratory, he worked on algorithms for parallel model checking, and a specification language for open systems, with a compiler that synthesizes implementations. He is a Postdoctoral Scholar in the Computing and Mathematical Sciences Department at Caltech.

 

CASE 2017 – Special Session on Model-Based Testing of Hybrid Systems

At the 13th IEEE Conference on Automation Science and Engineering, August 20-23, 2017, Wyndham Grand Hotel, Xi’an, China, two SyTeC colleagues, Knut Åkesson and Martin Fabian, organized, invited and chaired a special session on Model-Based Testing of Hybrid Systems. The presented papers were (presenters in bold):

  • Simulation of Hybrid Systems from Natural Language Specifications
    Oliveira, Bruno. Univ. Federal De Pernambuco
    Carvalho, Gustavo. Univ. Federal De Pernambuco
    Mousavi, Mohammad Reza. Halmstad Univ
    Sampaio, Augusto. Univ. Federal De Pernambuco
  • Objective Functions for Falsification of Signal Temporal Logic Properties in Cyber-Physical Systems
    Eddeland, Johan. Volvo Car Corp
    Miremadi, Sajed. Volvo Cars Corp
    Fabian, Martin. Chalmers Univ. of Tech
    Åkesson, Knut. Chalmers Univ. of Tech
  • Vacuity Aware Falsification for MTL Request-Response Specifications
    Dokhanchi, Adel. Arizona State Univ
    Yaghoubi, Shakiba. Arizona State Univ
    Hoxha, Bardh Southern. Illinois Univ
    Fainekos, Georgios. Arizona State Univ
  • Temporal Specification Testing of Hybrid Systems
    Dang, Thao. CNRS/VERIMAG
    Dreossi, Tommaso. Univ. of California, Berkeley

Conference website

Jan Tretmans – Model-Based Testing: There is Nothing More Practical than a Good Theory

Seminar: 25 April, 2017, 13:15, EF

Speaker: Jan Tretmans
TNO – Embedded Systems Innovation, Eindhoven, NL,
Radboud University, Nijmegen, NL,
Halmstad University, Halmstad, S.

We build ever larger and more complex software systems. Systematic testing plays an important role in assessing the quality of such systems. The effort for testing, however, turns out to grow even faster than the size and complexity of the systems under test themselves.One of the promising testing technologies to detect more bugs faster and cheaper is model-based testing. (more…)

Model-based testing starts with an abstract model of the system’s behaviour. This model constitutes a precise and concise specification of what the system shall do, and, consequently, is a good basis for the algorithmic generation of test cases and the analysis of test results. Model-based testing enables the next step in test automation by combining automatic test generation with test execution and providing more, longer, and more diversified test cases with less effort.

The presentation aims at covering the chain from theoretical concepts, via algorithms and tools, to industrial applications of model-based testing. Starting point is the ‘ioco’-testing theory for labelled transition systems, to which concepts from process algebra, the theoryof testing equivalences, symbolic transition systems, algebraic data types, satisfaction-modulo-theories tools, and equational reasoning are added. We show how these theories have led to the development of the model-based testing tool ‘TorXakis’.

On the one hand, TorXakis provides provably sound and exhaustive (in the limit) test generation from models. These models combine state-based control flow and complex data definitions, they deal with uncertainty through nondeterminism, they support compositionality by providing combinators for alternative, concurrent, sequential, exceptional, and interrupting behaviours, and they support abstraction and under-specification. On the other hand, TorXakis has shown practical usability in academia, both in research and in education,
as well as in industrial applications, ranging from smart-card software to large, systems-of-systems kind of applications. So, for model-based testing there is nothing more practical than a good theory.

Original announcement