scholarly journals Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems

10.29007/r74f ◽  
2020 ◽  
Author(s):  
Johan Lidén Eddeland ◽  
Alexandre Donzé ◽  
Sajed Miremadi ◽  
Knut Åkesson
Keyword(s):  
Temporal Logic ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Over Time ◽  
Requirement Models

In this benchmark proposal, we present a set of large specifications stated in Signal Temporal Logic (STL) intended for use in falsification of Cyber-Physical Systems. The main purpose of the benchmark is for tools that monitor STL specifications to be able to test their performance on complex specifications that have structure similar to industrial specifications. The benchmark itself is a Git repository which will therefore be updated over time, and new specifications can be added. At the time of submission, the repository contains a total of seven Simulink requirement models, resulting in 17 generated STL specifications.

scholarly journals ARCH-COMP 2019 Category Report: Falsification

10.29007/68dk ◽  
2019 ◽  
Author(s):  
Gidon Ernst ◽  
Paolo Arcaini ◽  
Alexandre Donzé ◽  
Georgios Fainekos ◽  
Logan Mathesen ◽  
...  
Keyword(s):  
Temporal Logic ◽  
State Of The Art ◽  
Cyber Physical Systems ◽  
The State ◽  
Base Line ◽  
Physical Systems ◽  
The Future ◽  
Friendly Competition ◽  
Initial Base

This report presents the results from the 2019 friendly competition in the ARCH workshop for the falsification of temporal logic specifications over Cyber-Physical Systems. We describe the organization of the competition and how it differs from previous years. We give background on the participating teams and tools and discuss the selected benchmarks and results. The benchmarks are available on the ARCH website1, as well as in the competition’s gitlab repository2. The main outcome of the 2019 competition is a common benchmark repository, and an initial base-line for falsification, with results from multiple tools, which will facilitate comparisons and tracking of the state-of-the-art in falsification in the future.

scholarly journals ARCH-COMP 2020 Category Report: Falsification

10.29007/trr1 ◽  
2020 ◽  
Author(s):  
Gidon Ernst ◽  
Paolo Arcaini ◽  
Ismail Bennani ◽  
Alexandre Donze ◽  
Georgios Fainekos ◽  
...  
Keyword(s):  
Temporal Logic ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Novel Approaches ◽  
Friendly Competition

This report presents the results from the 2020 friendly competition in the ARCH workshop for the falsification of temporal logic specifications over Cyber-Physical Systems. We briefly describe the competition settings, which have been inherited from the previous year, give background on the participating teams and tools and discuss the selected benchmarks. The benchmarks are available on the ARCH website1, as well as in the competition’s gitlab repository2. In comparison to 2019, we have two new participating tools with novel approaches, and the results show a clear improvement over previous performances on some benchmarks.

scholarly journals Timestamp Temporal Logic (TTL) for Testing the Timing of Cyber-Physical Systems

2017 ◽  
Vol 16 (5s) ◽  
pp. 1-20 ◽  
Author(s):  
Mohammadreza Mehrabian ◽  
Mohammad Khayatian ◽  
Aviral Shrivastava ◽  
John C. Eidson ◽  
Patricia Derler ◽  
...  
Keyword(s):  
Temporal Logic ◽  
Cyber Physical Systems ◽  
Physical Systems

Synthesis of Monitoring Rules with STL

2020 ◽  
Vol 29 (11) ◽  
pp. 2050177
Author(s):  
Sertac Kagan Aydin ◽  
Ebru Aydin Gol
Keyword(s):  
Genetic Algorithms ◽  
Web Services ◽  
Real Time ◽  
Temporal Logic ◽  
Online Monitoring ◽  
Cyber Physical Systems ◽  
Time Signal ◽  
Piecewise Constant ◽  
Physical Systems ◽  
Monitoring Algorithm

Online monitoring is essential to enhance the reliability for various systems including cyber-physical systems and Web services. During online monitoring, the system traces are checked against monitoring rules in real time to detect deviations from normal behaviors. In general, the rules are defined as boundary conditions by the experts of the monitored system. This work studies the problem of synthesizing online monitoring rules in the form of temporal logic formulas in an automated way. The monitoring rules are described as past-time signal temporal logic (ptSTL) formulas and an algorithm to synthesize such formulas from a given set of labeled system traces is proposed. The algorithm searches the formula space using genetic algorithms and produces the best formula representing a monitoring rule. In addition, online STL monitoring algorithm is improved to efficiently compute a quantitative valuation for piecewise-constant signals from ptSTL formulas, thus, to reduce the overhead of the real-time computation. The effectiveness of the results is shown on two illustrative examples inspired from online monitoring of Web services.

scholarly journals Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification

10.29007/f4vs ◽  
2020 ◽  
Author(s):  
Johan Lidén Eddeland ◽  
Sajed Miremadi ◽  
Knut Åkesson
Keyword(s):  
Objective Function ◽  
Temporal Logic ◽  
Simulation Models ◽  
Cyber Physical Systems ◽  
Objective Functions ◽  
Problem Statement ◽  
Testing Technique ◽  
Physical Systems ◽  
Simulation Based ◽  
Optimization Solvers

Temporal-logic based falsification of Cyber-Physical Systems is a testing technique used to verify certain behaviours in simulation models, however the problem statement typically requires some model-specific tuning of parameters to achieve optimal results. In this experience report, we investigate how different optimization solvers and objective functions affect the falsification outcome for a benchmark set of models and specifications. With data from the four different solvers and three different objective functions for the falsification problem, we see that choice of solver and objective function depends both on the model and the specification that are to be falsified. We also note that using a robust semantics of Signal Temporal Logic typically increases falsification performance compared to using Boolean semantics.

Sign in / Sign up

Export Citation Format

Share Document