Theoretical Foundations for Monitorability
Icelandic Research Fund Project nr. 163406-051 (2016-2018)
Status: Ongoing

The general aim of the project, which is led by Luca Aceto (Reykjavik University), Adrian Francalanza (University of Malta) and Anna Ingolfsdottir (Reykjavik University), is to develop further the theoretical foundations of monitorability for fragments of variants of Hennessy-Milner logic with recursion/modal mu-calculus.

The project work will build on the RV 2015 paper by the co-proposers, and on the experience developed during their previous work on runtime verification and on the tool detectEr. The goals of the project will be:

Researchers

The research team includes Luca Aceto (Reykjavik University, PI), Antonis Achilleos (Reykjavik University, postdoctoral researcher), Duncan Paul Attard (PhD student at the University of Malta, starting in February 2017), Ian Cassar (PhD student at the University of Malta), Adrian Francalanza (University of Malta, co-PI), Anna Ingolfsdottir (Reykjavik University, co-PI) and Guðmundur Stefansson (Reykjavik University, MSc student).

Project-related events (in reverse chronological order)

Publications

Books and edited volumes

  1. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(1):1--125, February 2017.
  2. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(2):127-242, March 2017.
  3. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(3):243--341, May 2017.
  4. Luca Aceto, Adrian Francalanza and Anna Ingolfsdottir (Eds.). Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016). EPTCS Vol. 208, 25 May 2016.
  5. Adrian Francalanza and Gordon J. Pace. Proceedings Second Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2017). EPTCS Vol. 254, July 2017.

Book chapters

  1. Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. A Runtime Monitoring Tool for Actor-Based Systems. In Behavioural Types: from Theory to Tools (Simon Gay and Antonio Ravara eds.), Chapter 3, pp. 49-76, River Publishers, 2017.

Journal papers

  1. Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner Logic with Recursion. Formal Methods in System Design, Springer, 2017. To appear. The official journal paper is here.

Conference and workshop papers

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. On the Complexity of Determinizing Monitors. Proceedings of 22nd International Conference Implementation and Application of Automata (CIAA 2017) (Arnaud Carayol and Cyril Nicaud eds.), Lecture Notes in Computer Science 10329, pp. 1-13, Springer, June 2017. [Official publisher version of the paper]
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. Monitoring for Silent Actions. Proceedings of FSTTCS 2017, the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, December 2017. To appear. [Authors' version]
  3. Antonis Achilleos. The Completeness Problem for Modal Logic. Proceedings of Symposium on LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS'18), Lecture Notes in Computer Science, Springer, December 2017. To appear. [arXiv version].
  4. Duncan Paul Attard and Adrian Francalanza. A Monitoring Tool for a Branching-Time Logic. Proceedings of Runtime Verification - 16th International Conference, RV 2016, Volume 10012 of Lecture Notes in Computer Science, pp. 473--481, Springer-Verlag, 2016.
  5. Duncan Paul Attard and Adrian Francalanza. Trace Partitioning and Local Monitoring for Asynchronous Components, Proceedings of 15th International Conference on Software Engineering and Formal Methods, SEFM 2017, Lecture Notes in Computer Science, Springer-Verlag, September 2017.
  6. Ian Cassar and Adrian Francalanza. On Implementing a Monitor-Oriented Programming Framework for Actor Systems. Proceedings of Integrated Formal Methods 2016 (iFM 2016), Volume 9681 of the series Lecture Notes in Computer Science, pp. 176-192, Springer-Verlag, June 2016.
  7. Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. eAOP - An Aspect Oriented Programming Framework for Erlang. Proceedings of the 16th ACM Erlang Workshop 2017, pp. 20-30, ACM Press 2017. [Authors' version]
  8. Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. A Survey of Runtime Monitoring Instrumentation Techniques. Proceedings of PrePost 2017, EPTCS, September 2017.
  9. Ian Cassar, Adrian Francalanza, Duncan Paul Attard, Luca Aceto and Anna Ingolfsdottir. A generic instrumentation tool for Erlang. Proceedings of RV-CuBES 2017 (International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools), Kalpa Publications in Computing, EasyChair, 2017.
  10. Ian Cassar, Adrian Francalanza, Duncan Paul Attard, Luca Aceto and Anna Ingolfsdottir. A Suite of Monitoring Tools for Erlang. Proceedings of RV-CuBES 2017 (International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools), Kalpa Publications in Computing, EasyChair, 2017.
  11. Adrian Francalanza. A Theory of Monitors. Proceedings of Foundations of Software Science and Computation Structures, Volume 9634 of the series Lecture Notes in Computer Science, pp. 145-161, Springer-Verlag, April 2016.
  12. Adrian Francalanza. Consistently-Detecting Monitors, Proceedings of the 28th International Conference on Concurrency Theory, CONCUR 2017, LIPIcs, September 2017.
  13. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica and Anna Ingólfsdóttir. A Foundation for Runtime Monitoring. Proceedings of Runtime Verification 2017, Lecture Notes in Computer Science 10548, pp. 8-29, Springer, September 2017.
  14. Vignir Gudmundsson, Mikael Lindvall, Luca Aceto, Johann Bergthorsson and Dharmalingam Ganesan. Model-based Testing of Mobile Systems – An Empirical Study on QuizUp Android App. Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016), Reykjavík, Iceland, 4th June 2016, Electronic Proceedings in Theoretical Computer Science 208, pp. 16–30. Published: 25th May 2016. [ArXiv]
  15. Annalizz Vella and Adrian Francalanza. Preliminary Results Towards Contract Monitorability. Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016), Reykjavík, Iceland, 4th June 2016, Electronic Proceedings in Theoretical Computer Science 208, pp. 54–63. Published: 25th May 2016. [ArXiv]

Other publications

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. The Complexity of Identifying Characteristic Formulas for muHML. Proceedings of PLS11 (11th Panhellenic Logic Symposium), July 2017.
  2. Luca Aceto and David de Frutos Escrig. Foreword for the special issue of Acta Informatica devoted to selected papers from CONCUR 2015. Acta Informatica, Springer, February 2017. The official published version can be freely viewed here.

Submitted papers

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. A Framework for Parameterized Monitorability. Submitted for conference publication.
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. Determinizing Monitors for HML with Recursion. Submitted for journal publication.

Pre-prints and Technical Reports

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. Determinizing Monitors for HML with Recursion. Version dated 30 November 2016, 53 pages.

Student theses

  1. Guðmundur Stefánsson. Work on new event sources for detectEr. MSc thesis, May 2017.
  2. Kari Tristan Helgason. Runtime Verification with DetectEr: a case study. Undergraduate research opportunity article at Reykjavik University. May 2015.
  3. Sævar Örn Kjartansson. The expressive power of deterministic monitors for muHML. Research-based BSc thesis in the Discrete Mathematics and Computer Science programme at Reykjavik University. December 2015.

Software tools

  1. detectErLITE
  2. detectEr for Java