Skip to content

Instantly share code, notes, and snippets.

@nikos-kekatos

nikos-kekatos/runtime_verification.md

Last active July 29, 2023 03:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save nikos-kekatos/e4b28b644fb2ca809334b399c1b38d50 to your computer and use it in GitHub Desktop.
Save nikos-kekatos/e4b28b644fb2ca809334b399c1b38d50 to your computer and use it in GitHub Desktop.
Download ZIP
Material for RV -- focusing on past-time
Raw
runtime_verification.md

Useful/Relevant Papers

Unorganized

Surveys/Good papers

  1. Runtime Verification for Decentralised and Distributed Systems, Adrian Francalanza, Jorge A. Perez, and Cesar Sanchez

    https://software.imdea.org/~cesar/papers/2018/rvbook/francalanza18runtime.pdf

    State of the art on distributed monitoring, survey, motivation, centralizeed vs decentralized, choreographed vs orchesrated

  2. A survey of challenges for runtime verification from advanced application domains (beyond software) https://link.springer.com/article/10.1007/s10703-019-00337-w

    survey paper, concentrate on application domains for RV, others than programming languages: Distributed systems, Hybrid and embedded systems, Hardware, Security and privacy, Transactional information systems, Contracts and policies, Huge, unreliable or approximated domains

  3. Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications https://link.springer.com/chapter/10.1007/978-3-319-75632-5_5 http://www-verimag.imag.fr/PEOPLE/maler/Papers/monitor-RV-chapter.pdf Monitoring Real Systems and Monitoring Simulated Models, Rigorous Specification Formalisms, Nice simple examples, STL, monitoring algorithms The satisfaction of a future formula by the whole sequence w is defined as its satisfaction at position 0 while that of a past formula, by its satisfaction at |w|. Past formulas have some advantages such as causality,

  4. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. http://www-verimag.imag.fr/~maler/Papers/STLRobustAlgo.pdf They present briefly an algorithm computing quantitative satisfaction of φ by 𝑤.

  5. Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. discussion about different interpretations of temporal logics over finite traces

  6. Introduction to Runtime Verification Ezio Bartocci, Yliès Falcone, Adrian Francalanza, Giles Reger https://hal.inria.fr/hal-01762297/file/book-chapter-introduction-to-RV.pdf https://link.springer.com/chapter/10.1007/978-3-319-75632-5_1#Sec7

  7. Runtime Verification of LTL on Lossy Traces Yogi Joshi, Guy Martin Tchamgoue, Sebastian Fischmeister https://uwaterloo.ca/embedded-software-group/sites/ca.embedded-software-group/files/uploads/files/sac2017-lossy-ltl.pdf

Past-time

  1. FOCETA specification language, Formal Specification for Learning-Enabled Autonomous Systems (FOMLAS) https://easychair.org/publications/preprint/3bws https://easychair.org/smart-slide/slide/wfFQ#
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment