Category Archives: Seminar

Licentiate Seminar Johan Lidén Eddeland – Falsification of signal-based specifications for cyber-physical systems – with applications from the automotive domain

January 21st, 2020, 10.00 – 12.00 in Room ED, EDIT-building.

Johan Lidén Eddeland is a PhD student at the Division of Systems and Control, Chalmers University of Technology

Discussion leader is Adjunct Professor Mattias Nyberg, Royal Institute of Technology, KTH, and Scania

Examiner is Professor Knut Åkesson

In the development of software for modern Cyber-Physical Systems, testing is an integral part that is rightfully given a lot of attention. Testing is done on many different abstraction levels, and especially for large-scale industrial systems, it can be difficult to know when the testing should conclude and the software can be considered correct enough for making its way into production. 
This thesis proposes new methods for analyzing and generating test cases as a means of being more certain that proper testing has been performed for the system under test. For analysis, the proposed approach includes automatically finding how much a given test suite has executed the physical properties of the simulated system.
For test case generation, an up-and-coming approach to find errors in Cyber-Physical Systems is simulation-based falsification. While falsification is suitable also for some large-scale industrial systems, sometimes there is a gap between what has been researched and what problems need to be solved to make the approach tractable in the industry. This thesis attempts to close this gap by applying falsification techniques to real-world models from Volvo Car Corporation, and adapting the falsification procedure where it has shortcomings for certain classes of systems. Specifically, the thesis includes a method for automatically transforming a signal-based specification into a formal specification in temporal logic, as well as a modification to the underlying optimization problem that makes falsification more viable in an industrial setting.
The proposed methods have been evaluated for both academic benchmark examples and real-world industrial models. One of the main conclusions is that the proposed additions and changes to analysis and generation of tests can be useful, given that one has enough information about the system under test. It is difficult to provide a general solution that will always work best — instead, the challenge lies in identifying which properties of the given system should be taken into account when trying to find potential errors in the system.

Link to thesis.

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.

Biography

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.

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.

Angela Wallenburg – Safe and Secure Programming Using SPARK

Seminar September 1, 12:15, EA

Speaker:  Angela Wallenburg, Altran, UK

Sometimes software really has to work. SPARK is a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed. By design, the SPARK language is immune to many programming language vulnerabilities (such as those listed by NIST/CWE/SANS). Under the hood, the SPARK static analysis tools use formal verification (automatic mathematical proof).

Generally, formal verification is rarely used in industry due to its high cost and level of skill required. However, over the past 25 years, SPARK has been applied worldwide in a range of industrial applications. A few examples include Rolls Royce Trent (engine control), EuroFighter Typhoon (military aircraft), and NATS iFACTS (air traffic control). Recently, SPARK has been attributed the reason of success for the Vermont Tech CubeSat, the only one of NASA’s 2013 launch of 12 mini satellites (ELaNa project) that remained operational until reentry.

During this talk, you will learn about the rationale of SPARK. We will cover topics such as strong typing, unambiguous semantics, modular verification, contracts, the verifying compiler, scalability, powerful static analysis, combination of test and proof, and cost-competitive development of software to regulations (such as DO-178C).

(original announcement)

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