Category Archives: Seminar

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