Search Results

Modern cyber-physical systems-of-systems (CPSoS) operate in complex systems-of-systems that must seamlessly work together to control safety- or mission-critical functions. Linear Temporal Logic (LTL) and Mission-time Linear Temporal logic (MLTL) ...

Runtime monitoring facilitates human oversight of safety-critical systems by collecting and aggregating data from sensors and other system components and by issuing alerts whenever the safety specification is violated. It is critical that the ...${}^{\mathrm{}}$${}^{\mathrm{}}$${}^{\mathrm{}}$${}^{\mathrm{}}$${}^{\mathrm{}}$

Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of ...

There is increasing use of artificial neural networks in Cyber-Physical Systems (CPS) such as autonomous vehicles (AVs). Here, convolutional neural networks (CNNs) are widely used for different types of computer-vision tasks. The complex nature of the ...

In dynamic runtime environments, like ooRexx applications, guard-locked multi-threaded applications may be deadlocked for many reasons. Breaking deadlocked code may yield the location of a deadlocked instruction but may not allow for identifying other ...

The dynamic programming language ooRexx includes a runtime monitoring keyword instruction named TRACE. This keyword instruction produces a trace line for each traced statement. Although additional trace information was added, ooRexx 5.0.0 is missing ...

Runtime verification (RV) is used to monitor executions of a system, checking them against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid a failure. One can identify two main ...

Runtime verification (RV) monitors program executions against formal specifications (specs). Researchers showed that RV during software testing amplifies the bug-finding ability of tests, and found hundreds of new bugs by using RV to monitor passing ...

This paper reports on the integration of runtime monitoring into fully-electric aircraft designed by Volocopter, a German aircraft manufacturer of electric multi-rotor helicopters. The runtime monitor recognizes hazardous situations and system ...

Runtime Verification (RV) is the process of taking a trace, representing an execution of some computational system, and checking it for satisfaction of some specification, written in a specification language. RV approaches are often aimed at being used ...

In runtime verification, manually formalizing a specification for monitoring system executions is a tedious and error-prone process. To address this issue, we consider the problem of automatically synthesizing formal specifications from system ...$$$$$$$$

Benchmarking software testing tools against known bugs is a classic approach to evaluating the tools’ bug finding abilities. However, this approach is difficult to give some clues on the tool-missed bugs to aid diagnosing the testing tools. As a result, ...

We present HyperMonitor a Python prototype of a novel runtime verification method specifically designed for predicting race conditions in multithread programs. Our procedure is based on the combination of Inductive Process Mining, Petri Net ...

Runtime verification (RV) is an effective lightweight formal method for improving software’s reliability at runtime. There exist no RV tools specially designed for C++ programs. This paper introduces the first one, i.e., CCMOP, which implements an ...

In the domain of video delivery, industrial software systems that produce multimedia streams are increasingly more complex. To ensure correctness of their behaviors, there is a strong need for verification and validation activities. In particular, ...

Robotic systems are increasingly integrated into various industries, including manufacturing, transportation, and healthcare. So, it is essential to identify the vulnerabilities of these systems and take precautions. These systems are vulnerable ...

Chatbots are here to stay, and are going to be deployed in various application domains. Unfortunately, amongst them, there are safety-critical ones. Thus, we need a way to guarantee our chatbots will always behave as expected. In this paper, we ...

Application development for the modern Web involves sophisticated engineering workflows which include user interface aspects. Those involve Web elements typically created with HTML/CSS markup and JavaScript-like languages, yielding Web documents. ...

Software systems are hard to trust, especially when autonomous. To overcome this, formal verification techniques can be deployed to verify such systems behave as expected. Runtime Verification is one of the most prominent and lightweight ...

Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set ...$$