, Patterns Project, 1999.
, Patterns Project: List of specifications, 1999.
Comparing Finite-State Verification Techniques for Concurrent Software, 1999. ,
Sampling-based Decentralized Monitoring for Networked Embedded Systems, Proceedings Third International Workshop on Hybrid Autonomous Systems, HAS 2013, vol.124, pp.85-99, 2013. ,
, Lectures on Runtime Verification -Introductory and Advanced Topics, Lecture Notes in Computer Science, vol.10457, 2018.
First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014, International Journal on Software Tools for Technology Transfer, pp.1-40, 2017. ,
URL : https://hal.archives-ouvertes.fr/cea-01845191
Failure-aware Runtime Verification of Distributed Systems, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, vol.45, pp.590-603, 2015. ,
Decentralised LTL monitoring, Formal Methods in System Design, vol.48, pp.46-93, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-00857286
Runtime Verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol, vol.20, p.14, 2011. ,
Decentralised LTL Monitoring, FM 2012: Formal Methods -18th International Symposium, vol.7436, pp.85-100, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00857286
Challenges in Fault-Tolerant Distributed Runtime Verification, pp.363-370, 2016. ,
The Complexity of Boolean Formula Minimization, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games (Lecture Notes in Computer Science), vol.5125, pp.24-35, 2008. ,
Organising LTL Monitors over Distributed Systems with a Global Clock, Runtime Verification -5th International Conference, vol.8734, pp.140-155, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01120551
Organising LTL monitors over distributed systems with a global clock, Formal Methods in System Design, vol.49, pp.109-158, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01120551
A Data Flow Monitoring Service Based on Runtime Verification for AUTOSAR, 14th IEEE International Conference on High Performance Computing and Communication & 9th IEEE International Conference on Embedded Software and Systems, HPCC-ICESS 2012, pp.1508-1515, 2012. ,
LOLA: Runtime Monitoring of Synchronous Systems, 12th International Symposium on Temporal Representation and Reasoning (TIME 2005, pp.166-174, 2005. ,
Rapidly Adjustable Non-intrusive Online Monitoring for Multi-core Systems, Formal Methods: Foundations and, pp.179-196, 2017. ,
Topology, monitorable properties and runtime verification, Theoretical Aspects of Computing, vol.537, pp.29-41, 2014. ,
On Distributed Monitoring of Asynchronous Systems, Logic, Language, Information and Computation -19th International Workshop, vol.7456, pp.70-84, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00825771
Manipulating LTL formulas using Spot 1.0, Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), vol.8172, pp.442-445, 2013. ,
Patterns in Property Specifications for Finite-State Verification, Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, pp.411-420, 1999. ,
Monitoring Decentralized Specifications, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.125-135, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01653725
THEMIS: A Tool for Decentralized Monitoring Algorithms, Proceedings of 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'17-DEMOS), 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01653727
, , 2017.
, THEMIS Article Artifact, 2018.
You Should Better Enforce Than Verify, Runtime Verification -First International Conference, RV 2010, St. Julians, Malta, vol.6418, pp.89-105, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00523653
Efficient and Generalized Decentralized Monitoring of Regular Languages, Formal Techniques for Distributed Objects, Components, and Systems -34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, vol.8461, pp.66-83, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00972559
What can you verify and enforce at runtime? STTT, vol.14, pp.349-382, 2012. ,
NATO science for peace and security series, d: information and communication security, Engineering Dependable Software Systems, vol.34, pp.141-175, 2013. ,
A Taxonomy for Classifying Runtime Verification Tools, Runtime Verification -18th International Conference, vol.11237, pp.241-262, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01882410
Runtime Failure Prevention and Reaction, pp.103-134, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01723606
Runtime Verification for Decentralised and Distributed Systems, pp.176-210, 2018. ,
When RV Meets CEP, pp.68-91, 2016. ,
Event Stream Processing with Multiple Threads, pp.359-369, 2017. ,
An Overview of AspectJ, ECOOP 2001 -Object-Oriented Programming, 15th European Conference, vol.2072, pp.327-353, 2001. ,
Formally specified monitoring of temporal properties, 11th Euromicro Conference on Real-Time Systems (ECRTS 1999, pp.114-122, 1999. ,
A brief account of runtime verification, J. Log. Algebr. Program, vol.78, pp.293-303, 2009. ,
Runtime Verification for Interconnected Medical Devices, pp.380-387, 2016. ,
, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications -7th International Symposium, vol.9953, 2016.
Decentralized Runtime Verification of LTL Specifications in Distributed Systems, 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp.494-503, 2015. ,
Efficient abstraction algorithms for predicate detection, Theor. Comput. Sci, vol.688, pp.24-48, 2017. ,
Detecting Temporal Logic Predicates on Distributed Computations, DISC 2007, Proceedings (Lecture Notes in Computer Science), Andrzej Pelc, vol.4731, pp.420-434, 2007. ,
PSL Model Checking and Run-Time Verification Via Testers, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, vol.4085, pp.573-586, 2006. ,
Rewriting-Based Techniques for Runtime Verification, Autom. Softw. Eng, vol.12, pp.151-197, 2005. ,
Three-valued asynchronous distributed runtime verification, Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp.52-61, 2014. ,
Efficient Decentralized Monitoring of Safety in Distributed Systems, 26th International Conference on Software Engineering, pp.418-427, 2004. ,
Conflict-Free Replicated Data Types, Stabilization, Safety, and Security of Distributed Systems -13th International Symposium, vol.6976, pp.386-400, 2011. ,
URL : https://hal.archives-ouvertes.fr/inria-00609399
Depth-First Search and Linear Graph Algorithms, SIAM J. Comput, vol.1, pp.146-160, 1972. ,
, The Chiron Team. Chiron User Interface, 1999.
Monitoring Algorithms for Metric Temporal Logic Specifications, Electronic Notes in Theoretical Computer Science, vol.113, pp.145-162, 2005. ,
A Bridging Model for Parallel Computation, Commun. ACM, vol.33, pp.103-111, 1990. ,
Efficient Solutions to the Replicated Log and Dictionary Problems, Operating Systems Review, vol.20, pp.57-66, 1986. ,
, We note that, since the automaton is deterministic, there is a unique q i+1 such that q i+1 = ?(q i , evt i+1 )
In this section, we present the setup phase. As such, we present the generation of the decentralized specification from a start LTL formula. Choreography begins by taking the main formula, then deciding to split it into subformulas. Each monitor will monitor the subformula, notify other monitors of its verdict, and when needed respawn . Recall from the definition of ? ? (see Definition 5.4), that monitoring is recursively applied to the remainder of a trace starting at the current event. That is ,
, ? A id the automaton that monitors the subformula
Mons the monitors that this monitor should notify of a verdict ,
Mons the monitors that send their verdicts to this monitor ,