Article
Computer Science, Hardware & Architecture
Marcel Mettler, Daniel Mueller-Gritschneder, Ulf Schlichtmann
Summary: This article presents a decentralized monitoring architecture for large-scale multi-tile MPSoCs, along with a lightweight hardware solution to reduce the performance and power overhead of RV. A new tracing interconnect and an integer linear programming algorithm are used for the assignment of requirements to monitors.
ACM TRANSACTIONS ON ARCHITECTURE AND CODE OPTIMIZATION
(2021)
Article
Computer Science, Theory & Methods
Daniel Selvaratnam, Michael Cantoni, J. M. Davoren, Iman Shames
Summary: This paper introduces a method for verifying continuous-time polynomial spline trajectories against linear temporal logic specifications by sampling trajectories to generate discrete traces for path checking. It also provides general topological conditions to ensure the recording of traces for arbitrary continuous paths and region descriptions.
THEORETICAL COMPUTER SCIENCE
(2022)
Article
Computer Science, Software Engineering
Klaus Havelund, Doron Peled
Summary: Linear temporal logic (LTL) is widely used in formal methods, with various extensions proposed to enhance its expressiveness, albeit with limited adoption in practice. This paper introduces extensions of propositional LTL and first-order LTL with rules for runtime verification, focusing on past time versions. The proposed monitoring algorithm for the extension of past time first-order LTL with rules is implemented and experimental results are provided.
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
(2021)
Article
Computer Science, Information Systems
Luis Miguel Danielsson, Cesar Sanchez
Summary: - We study the problem of monitoring distributed systems and propose a solution to monitor decentralized systems using stream runtime verification specifications.
- We describe the monitoring problem for timed-asynchronous networks and provide a decentralized algorithm along with proofs of its correctness.
Article
Computer Science, Information Systems
Zhe Yang, Meiyi Dai, Jian Guo
Summary: Smart contracts are crucial for blockchain applications, but they often face security issues. This paper proposes a formal verification method to ensure the correctness and credibility of smart contracts in Ethereum transactions.
Article
Computer Science, Theory & Methods
Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, Martin Zimmermann
Summary: Runtime monitoring is commonly used to detect violations of desired properties in systems, but some approaches may not be able to monitor all formulas effectively. Recent introduction of robust semantics captures varying degrees of property violations, showing potential in monitoring applications.
FORMAL METHODS IN SYSTEM DESIGN
(2021)
Article
Computer Science, Hardware & Architecture
Paul Naert, Seyed Vahid Azhari, Michel Dagenais
Summary: The paper introduces a new framework for building efficient and targeted dynamic RV tools, bridging the gap between dynamic heavy-weight tools and lighter and more efficient static tools. The framework is divided into source and binary domains, providing a user interface and debugger for users and developers to easily adjust and adapt tools.
JOURNAL OF SYSTEMS ARCHITECTURE
(2021)
Article
Computer Science, Software Engineering
Adriano Torres, Pedro Costa, Luis Amaral, Jonata Pastro, Rodrigo Bonifacio, Marcelo d'Amorim, Owolabi Legunsen, Eric Bodden, Edna Dias Canedo
Summary: This article investigates runtime verification as an alternative method for detecting crypto API misuse. The results show that runtime verification has higher accuracy compared to static analyzers, and can be combined with static analysis to improve detection effectiveness.
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
(2023)
Article
Engineering, Electrical & Electronic
Yunus Sabri Kirca, Elif Degirmenci, Zekeriyya Demirci, Ahmet Yazici, Metin Ozkan, Salih Ergun, Alper Kanak
Summary: Robotic systems have become increasingly important in various fields, and ensuring their safety and security is crucial. This study proposes a runtime verification approach for anomaly detection in the robot operating system (ROS). An anomaly detection method is developed to detect unexpected situations, and a holistic runtime verification architecture is proposed. Experimental results demonstrate the feasibility of the proposed architecture for different anomaly detection algorithms.
Article
Computer Science, Information Systems
Haoyu Luo, Xiao Liu, Jin Liu, Yun Yang, John Grundy
Summary: This article proposes a new approach to automatically verify the temporal conformance of parallel workflow instances in a cloud environment. Instead of using response time, workflow throughput is employed as the performance measurement to efficiently monitor a large number of parallel workflow instances. The proposed strategy takes into account the effect of time delay propagation in cloud workflow systems to accurately verify workflow runtime temporal conformance.
IEEE TRANSACTIONS ON SERVICES COMPUTING
(2022)
Article
Computer Science, Hardware & Architecture
Xiaoning Du, Alwen Tiu, Kun Cheng, Yang Liu
Summary: The article introduces the use of Metric Linear-Time Logic (MTL) based policy languages for runtime malware or intrusion detection applications. It proposes a past-time variant of MTL extended with an aggregate operator to specify qualitative and quantitative policies. By adding the aggregate operator, policies based on the number of times sub-policies are satisfied within a specified past time interval can be monitored independently of the length of system event traces.
IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING
(2021)
Proceedings Paper
Computer Science, Hardware & Architecture
Anastasios Temperekidis, Nikolaos Kekatos, Panagiotis Katsaros
Summary: This study introduces a technical approach for runtime verification of properties for the entire co-simulated system. By integrating the DejaVU monitor synthesis tool at the master algorithm level of FMI-based co-simulation, predicates and events from all constituents of a simulated system can be monitored. Runtime monitors can also be used as a means to control the co-simulation run.
RUNTIME VERIFICATION (RV 2022)
(2022)
Article
Engineering, Aerospace
Saswata Paul, Elkin Cruz, Airin Dutta, Ankita Bhaumik, Erik Blasch, Gul Agha, Stacy Patterson, Fotis Kopsaftopoulos, Carlos Varela
Summary: This article introduces the ASSURE framework, which uses formal methods for the verification of safety-critical aerospace systems. It supports the verification of deterministic and nondeterministic properties of distributed and centralized applications using formal theorem proving tools. The framework includes verifiable algorithms, software, formal reasoning models, proof libraries, and a data-driven runtime verification approach for provably safe Internet of Planes infrastructure.
IEEE AEROSPACE AND ELECTRONIC SYSTEMS MAGAZINE
(2023)
Article
Computer Science, Software Engineering
Marco Robol, Travis D. Breaux, Elda Paja, Paolo Giorgini
Summary: Advances in personalization of digital services are driven by low-cost data collection and processing, as well as a wide variety of third-party frameworks. New privacy regulations, such as GDPR and the California Consumer Privacy Act, require organizations to explicitly state their data practices in privacy policies. To ensure GDPR compliance in the face of evolving consent practices, a formal consent framework is proposed that supports retroactive and non-retroactive granting and withdrawal of consent, and includes a reasoning framework, a scripting language, consent evolution use cases, and a scalability evaluation. The framework can be integrated into a runtime architecture to monitor policy violations as data practices evolve.
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY
(2023)
Article
Mathematical & Computational Biology
Ge Zhou, Chunzheng Yang, Peng Lu, Xi Chen
Summary: This paper presents a method that learns a probabilistic model of the system and environment from historical traces and generates a probabilistic runtime monitor to quantitatively predict the satisfaction of temporal properties. By generating the product of DTMC and DRA and computing the probabilities for each state, early warnings can be given and adjustments can be made in advance.
MATHEMATICAL BIOSCIENCES AND ENGINEERING
(2022)