TP-DejaVu: Combining Operational and Declarative Runtime Verification
Runtime verification (RV) facilitates monitoring the executions of a system, comparing them against a formal specification. A main challenge is to keep the incremental complexity of updating its internal structure, each time a new event is inspected, to a minimum. There is a tradeoff between achieving a low incremental complexity and the expressive power of the used specification formalism. We seek an RV tool that allows us to specify properties of executions that include data, with the possibility to apply arithmetic operations and comparisons on the data values. In order to be able to apply efficient RV for specifications with these capabilities we combine two RV methodologies: the first one is capable of performing arithmetic operations and comparisons based on the most recent events; the second is capable of handling many events with data and relating between events that occur at arbitrary distance in the observed execution. This is done by two phase RV, where the first phase makes the arithmetic calculations and comparisons and feeds the second phase with augmented events for further processing. This is implemented as a tool called TP-DejaVu (where TP stands for two phase), which extends the DejaVu tool.
Mon 15 JanDisplayed time zone: London change
16:00 - 17:30 | Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room Chair(s): Helmut Seidl Technische Universität München | ||
16:00 20mTalk | Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability VMCAI Pre-print | ||
16:20 20mTalk | Parameterized Verification of Disjunctive Timed NetworksRecorded VMCAI Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA | ||
16:40 20mTalk | Resilience and Home-Space for WSTS VMCAI | ||
17:00 20mTalk | Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic VMCAI Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp Pre-print | ||
17:20 10mTalk | TP-DejaVu: Combining Operational and Declarative Runtime Verification VMCAI Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki |