Skip to main content
SpringerLink
Log in

Towards Probabilistic Session-Type Monitoring

  • Conference paper
  • First Online:
Coordination Models and Languages (COORDINATION 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12717))

Included in the following conference series:

Abstract

We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is augmented with a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviates from the one specified by the probabilistic session type.

The work has been partly supported by: the project MoVeMnt (No: 217987-051) under the Icelandic Research Fund; the BehAPI project funded by the EU H2020 RISE under the Marie Skłodowska-Curie action (No: 778233); the MIUR projects PRIN 2017FTXR7S IT MATTERS and 2017TWRCNB SEDUCE; the EU Horizon 2020 project 830929 CyberSec4Europe; the Danish Industriens Fonds Cyberprogram 2020-0489 Security-by-Design in Digital Denmark.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This design is conveniently inherited from [4, 5] but is orthogonal to our approach.

References

  1. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1–52:29 (2019). https://doi.org/10.1145/3290365

    Article  Google Scholar 

  2. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: An operational guide to monitorability with applications to regular properties. Softw. Syst. Model. 20(2), 335–361 (2021). https://doi.org/10.1007/s10270-020-00860-z

    Article  Google Scholar 

  3. Agresti, A., Hitchcock, D.B.: Bayesian inference for categorical data analysis. Stat. Methods Appl. 14(3), 297–330 (2005). https://doi.org/10.1007/s10260-005-0121-y

    Article  MathSciNet  MATH  Google Scholar 

  4. Bartolo Burlò, C., Francalanza, A., Scalas, A.: On the monitorability of session types, in theory and practice. In: 35th European Conference on Object-Oriented Programming, ECOOP 2021, 12–17 July 2021 (2021, to appear)

    Google Scholar 

  5. Bartolo Burlò, C., Francalanza, A., Scalas, A.: Towards a hybrid verification methodology for communication protocols (short paper). In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 227–235. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50086-3_13

    Chapter  Google Scholar 

  6. Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33–58 (2017). https://doi.org/10.1016/j.tcs.2017.02.009

    Article  MathSciNet  MATH  Google Scholar 

  7. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983). https://doi.org/10.1145/322374.322380

    Article  MathSciNet  MATH  Google Scholar 

  8. Das, A., Wang, D., Hoffmann, J.: Probabilistic resource-aware session types. CoRR abs/2011.09037 (2020). https://arxiv.org/abs/2011.09037

  9. Dawes, J.H., Reger, G.: Explaining violations of properties in control-flow temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 202–220. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_12

    Chapter  Google Scholar 

  10. Esparza, J., Kiefer, S., Kretínský, J., Weininger, M.: Online monitoring \(\omega \)-regular properties in unknown Markov chains. CoRR abs/2010.08347 (2020). https://arxiv.org/abs/2010.08347

  11. Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75–99 (2016). https://doi.org/10.1109/TSE.2015.2421318

    Article  Google Scholar 

  12. Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 314–319. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_30

    Chapter  Google Scholar 

  13. Francalanza, A.: A theory of monitors. Inf. Computa. 104704 (2021, to appear). https://doi.org/10.1016/j.ic.2021.104704

  14. Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87–116 (2017). https://doi.org/10.1007/s10703-017-0273-z

    Article  MATH  Google Scholar 

  15. Francalanza, A., Cini, C.: Computer says no: verdict explainability for runtime monitors using a local proof system. J. Log. Algebraic Methods Program. 119, 100636 (2021). https://doi.org/10.1016/j.jlamp.2020.100636

    Article  MathSciNet  MATH  Google Scholar 

  16. Francalanza, A., Mezzina, C.A., Tuosto, E.: Towards choreographic-based monitoring. In: Ulidowski, I., Lanese, I., Schultz, U.P., Ferreira, C. (eds.) RC 2020. LNCS, vol. 12070, pp. 128–150. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-47361-7_6

    Chapter  Google Scholar 

  17. Gommerstadt, H., Jia, L., Pfenning, F.: Session-typed concurrent contracts. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 771–798. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_27

    Chapter  Google Scholar 

  18. Grunske, L.: An effective sequential statistical test for probabilistic monitoring. Inf. Softw. Technol. 53(3), 190–199 (2011). https://doi.org/10.1016/j.infsof.2010.10.003

    Article  Google Scholar 

  19. Inverso, O., Melgratti, H.C., Padovani, L., Trubiani, C., Tuosto, E.: Probabilistic analysis of binary sessions. In: CONCUR. LIPIcs, vol. 171, pp. 14:1–14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.14

  20. Newcombe, R.G.: Confidence Intervals for Proportions and Related Measures of Effect Size. CRC Biostatistics Series. CRC Press, Chapman & Hall, Boca Raton (2012)

    Book  Google Scholar 

  21. Ruchkin, I., Sokolsky, O., Weimer, J., Hedaoo, T., Lee, I.: Compositional probabilistic analysis of temporal properties over stochastic detectors. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 39(11), 3288–3299 (2020). https://doi.org/10.1109/TCAD.2020.3012643

    Article  Google Scholar 

  22. Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: ECOOP. LIPIcs, vol. 56, pp. 21:1–21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.ECOOP.2016.21

  23. Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000). https://doi.org/10.1145/353323.353382

    Article  Google Scholar 

  24. Stoller, S.D., et al.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_15

    Chapter  Google Scholar 

  25. Wilson, E.B.: Probable inference, the law of succession, and statistical inference. J. Am. Stat. Assoc. 22(158), 209–212 (1927). https://www.tandfonline.com/doi/abs/10.1080/01621459.1927.10502953

  26. Zhu, Y., Xu, M., Zhang, P., Li, W., Leung, H.: Bayesian probabilistic monitor: a new and efficient probabilistic monitoring approach based on Bayesian statistics. In: QSIC, pp. 45–54. IEEE (2013). https://doi.org/10.1109/QSIC.2013.55

Download references

Author information

Authors and Affiliations

  1. Gran Sasso Science Institute, L’Aquila, Italy

    Christian Bartolo Burlò, Catia Trubiani & Emilio Tuosto

  2. Department of Computer Science, University of Malta, Msida, Malta

    Adrian Francalanza

  3. DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

    Alceste Scalas

Authors
  1. Christian Bartolo Burlò
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alceste Scalas
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Catia Trubiani
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Emilio Tuosto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christian Bartolo Burlò .

Editor information

Editors and Affiliations

  1. University of Turin, Turin, Italy

    Ferruccio Damiani

  2. Sir Alwyn William Building, University of Glasgow, Glasgow, UK

    Ornela Dardha

Rights and permissions

Reprints and permissions

Copyright information

© 2021 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bartolo Burlò, C., Francalanza, A., Scalas, A., Trubiani, C., Tuosto, E. (2021). Towards Probabilistic Session-Type Monitoring. In: Damiani, F., Dardha, O. (eds) Coordination Models and Languages. COORDINATION 2021. Lecture Notes in Computer Science(), vol 12717. Springer, Cham. https://doi.org/10.1007/978-3-030-78142-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-78142-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-78141-5

  • Online ISBN: 978-3-030-78142-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation