8 papers
Practical Runtime Enforcement of First-Order Temporal Requirements
François Hublet, David Basin, Srđan Krstić
Runtime enforcers observe a system's behavior and exert control over it to ensure that the system always adheres to its requirements. Many natural requirements not only formulate r…
Towards an Enforceable GDPR Specification
François Hublet, Alexander Kvamme, Srđan Krstić
While Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's GDPR, achieving PbD in real software systems is a notoriously difficult task. One emergin…
COST Action IC 1402 ArVI: Runtime Verification Beyond Monitoring -- Activity Report of Working Group 1
Wolfgang Ahrendt, Cyrille Artho, Christian Colombo +9
This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of th…
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
César Sánchez, Gerardo Schneider, Wolfgang Ahrendt +13
Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime…
Efficient Large-scale Trace Checking Using MapReduce
Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi +2
The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL…
InstaCluster: Building A Big Data Cluster in Minutes
Giovanni Paolo Gibilisco, Srdan Krstic
Deploying, configuring, and managing large clusters is very a demanding and cumbersome task due to the complexity of such systems and the variety of skills needed. One needs to per…
Offline Trace Checking of Quantitative Properties of Service-Based Applications
Domenico Bianculli, Carlo Ghezzi, Srdan Krstic +1
Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each pa…
Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce
Domenico Bianculli, Carlo Ghezzi, Srdan Krstic
Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the syst…