Author Archives: admin

Licentiate Seminar Zahra Ramezani – Enhancing Temporal Logic Falsification of Cyber-Physical Systems

When: 6th of November at 13.15 on Zoom.
Where: Join the seminar from PC, Mac, Linux, iOS or Android via zoom

E-mail in advance to get the password

The seminar can be accessed through Zoom, and it will open shortly before 13.15. We would kindly ask you to keep the video off and mute the microphone during the seminar. At the end of the session, there will be an opportunity to ask questions through Zoom. In case there will be any updates about the event, these will be posted on this website.

Zahra Ramezani is a PhD student at the Division of Systems and Control​, research group of Automation
Discussion leader is Professor Mohammad Mousavi, Leicester University, UK
Examiner is Professor Knut Åkesson, Division of Systems and Control​

Cyber-physical systems (CPSs) are engineering systems that bridge the cyber-world of communications and computing with the physical world. These systems are usually safety-critical and exhibit both discrete and continuous dynamics that may have complex behavior. Typically, these systems have to satisfy given specifications, i.e., properties that define the valid behavior. One commonly used approach to evaluate the correctness of CPSs is testing. The main aim of testing is to detect if there are situations that may falsify the specifications.

For many industrial applications, it is only possible to simulate the system under test because mathematical models do not exist, thus formal verification is not a viable option. Falsification is a strategy that can be used for testing CPSs as long as the system can be simulated and formal specifications exist. Falsification attempts to find counterexamples, in the form of input signals and parameters, that violate the specifications of the system. Random search or optimization can be used for the falsification process. In the case of an optimization-based approach, a quantitative semantics is needed to associate a simulation with a measure of the distance to a specification being falsified. This measure is used to guide the search in a direction that is more likely to falsify a specification, if possible.

The measure can be defined in different ways. In this thesis, we evaluate different quantitative semantics that can be used to define this measure. The efficiency of the falsification can be affected by both the quantitative semantics used and the choice of the optimization method. The presented work attempts to improve the efficiency of the falsification process by suggesting to use multiple quantitative semantics, as well as a new optimization method. The use of different quantitative semantics and the new optimization method have been evaluated on standard benchmark problems. We show that the proposed methods improve the efficiency of the falsification process.

Keywords: Cyber-Physical Systems, Testing, Falsification

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).

Volvo – 1st Workshop on Automatic Generation of Test Cases for Mechatronic Systems

Workshop: September 5, 13:00-16:00, Volvo Car Corporation

With the rapidly increasing complexity of the mechatronic systems in the automotive industry, it is very hard to reach a sufficient level of test coverage during software testing in different test environments. In near future, it will be almost impossible to only rely on manually generated test cases!

In this workshop, we will present the latest results that have been achieved by integrating new tools and methodologies in the software development chain at Vehicle Propulsion (electric drive, traction battery, charging and combustion engine), in an attempt to assist the test engineers by automatically generating test cases. We will also talk about the next steps in this area. Our ambition is to have a quite interactive session with a lot of questions and discussions. We hope that as many of you can participate from different areas in order to find synergies, exchange information and together drive this area forward.

Relevant target groups include, but are not limited to, software testers, software developers, requirement engineers, technical leaders, and managers.

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)