Category Archives: Guest Researcher

Seminar: Temporal Logic Falsification of Cyber-Physical Systems: An Input-Signal-Space Optimization Approach

Thursday 16th May, 15:15 in EDIT 8103
Prof. Michel Reniers, Eindhoven University of Technology

Temporal logic falsification is a promising approach to model-based testing of cyber-physical systems. It starts off with a formalized system requirement specified as a Metric Temporal Logic (MTL) property. Subsequently, test input signals are generated in order to stimulate the system and produce an output signal. Finally, output signals of the system under test are compared to those prescribed by the property to falsify the property by means of a counterexample. To find such a counterexample, Markov Chain Monte-Carlo (MCMC) methods are used to construct an optimization problem to steer the test input generations to those input areas that maximize the probability of falsifying the property. In this paper, we identify two practical issues in the above-mentioned falsification process. Firstly, a fixed time domain of the input-signal space is assumed in this process, which restricts the frequency content of the (generated) input signals. Secondly, the existing process allows for input selection steered by the distribution of a single input variable. We address these issues, by firstly, considering multiple time domains for input-signal space. Subsequently, an input-signal-space optimization problem is formally defined and implemented in S-TaLiRo+, an extension of S-TaLiRo (an existing implementation for solving the MTL falsification problem). Secondly, we propose a decoupled scheme that considers the distribution of each input variable independently. The applicability of the proposed solutions are experimentally evaluated on well-known benchmark problems.

This is joint work with Arend Aerts, Bryan Tong Minh, and Mohammad Reza Mousavi and was published in A-MOST (2018).

Seminar – Testing Safety PLCs with QuickCheck

Wednesday 30 Jan 13:15 in ED

David Thönnessen

Testing safety-related industrial systems is usually carried out on the basis of checklists. A tester has a list of scenarios that he manually applies to the system and checks whether the system behaves according to its specification. Operators behave unpredictably. Their behavior may not be covered by the set of scenarios tested and may lead to dangerous situations. To avoid this, randomized test case generation can be useful as it allows for a huge number of different scenarios. The presented framework utilizes a tool for randomized test case generation, QuickCheck, to trigger event sequences that are then applied to a safety PLC. Evaluations show that this concept is capable of finding errors in safety implementations or increasing the tester’s confidence in the correctness of the code by a large number of passed test cases. While this concept points out to be powerful, it does not require much effort of the tester as the execution of test cases does not require user interaction.

Slides are available here.


David Thönnessen received the B.Sc. degree (2012) and the M.Sc. degree (2014) from the Department of Computer Science at RWTH Aachen University, Germany. Since 2014, he is a research assistant at the Chair of Computer Science 11 – Embedded Software at RWTH Aachen University with the focus on model-based testing of control systems in industry.

He is currently a guest researcher with the Department of Signals and Systems at Chalmers University of Technology for the period of August 2018 to January 2019.

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.