Category Archives: Uncategorized

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 PhdAdm.e2@chalmers.se 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​

Abstract
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

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.