TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic Specifications

被引：10

作者：

Cralley, Joseph ^{[1
]}

Spantidi, Ourania ^{[1
]}

Hoxha, Bardh ^{[2
]}

Fainekos, Georgios ^{[3
]}

机构：

[1] Southern Illinois Univ, Carbondale, IL 62901 USA

[2] Toyota Res Inst North Amer, Ann Arbor, MI 48105 USA

[3] Arizona State Univ, Tempe, AZ 85281 USA

来源：

RUNTIME VERIFICATION (RV 2020) | 2020年 / 12399卷

关键词：

Testing; Temporal logic; Robustness; SYSTEMS; FALSIFICATION; VERIFICATION;

D O I：

10.1007/978-3-030-60508-7_22

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents the Temporal Logic Toolkit (TLTk), a modular falsification tool for signal temporal logic specifications developed in Python and C. At the core of the tool, an algorithm for robustness computation is utilized that supports multi-threaded CPU/GPU computation. The tool enables memory-efficient, parallel, robustness computation of system traces. In addition, the python implementation enables the addition and modification of temporal operators for application-specific scenarios. The performance of the tool is evaluated against state-of-the-art robustness computation engines DP-TaLiRo and Breach on a number of benchmark problems.

引用

页码：404 / 416

页数：13

共 50 条

[1] Robustness of temporal logic specifications
Fainekos, Georgios E.
Pappas, George J.
[J]. FORMAL APPROACHES TO SOFTWARE TESTING AND RUNTIME VERIFICATION, 2006, 4262 : 178 - +
[2] Temporal Robustness of Temporal Logic Specifications: Analysis and Control Design
Rodionova, Alena
Lindemann, Lars
Morari, Manfred
Pappas, George
[J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2023, 22 (01)
[3] Robustness of temporal logic specifications for continuous-time signals
Fainekos, Georgios E.
Pappas, George J.
[J]. THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4262 - 4291
[4] USING TEMPORAL LOGIC SPECIFICATIONS TO DEBUG PARALLEL PROGRAMS
FREY, M
WEININGER, A
[J]. MICROPROCESSING AND MICROPROGRAMMING, 1993, 39 (2-5): : 97 - 100
[5] Testing parallel and distributed programs with temporal logic specifications
Frey, M
Oberhuber, M
[J]. SECOND INTERNATIONAL WORKSHOP ON SOFTWARE ENGINEERING FOR PARALLEL AND DISTRIBUTED SYSTEMS, PROCEEDINGS, 1997, : 62 - 72
[6] Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures
Rizk, Aurelien
Batt, Gregory
Fages, Francois
Soliman, Sylvain
[J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (26) : 2827 - 2839
[7] A temporal logic of robustness
French, Tim
McCabe-Dansted, John C.
Reynolds, Mark
[J]. FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 193 - +
[8] Robust control for signal temporal logic specifications using discrete average space robustness
Lindemann, Lars
Dimarogonas, Dimos V.
[J]. AUTOMATICA, 2019, 101 : 377 - 387
[9] Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications
Mehdipour, Noushin
Vasile, Cristian-Ioan
Belta, Calin
[J]. 2019 AMERICAN CONTROL CONFERENCE (ACC), 2019, : 1690 - 1695
[10] Composition of temporal logic specifications
Alexander, A
[J]. APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 98 - 116

← 1 2 3 4 5 →