Skip to main content
SpringerLink
Log in

Operational Semantics of Process Monitors

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

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

Included in the following conference series:

  • 1236 Accesses

Abstract

\(\text {CSP}_E\) is a specification language for runtime monitors that can directly express concurrency in a bottom-up manner that composes the system from simpler, interacting components. It includes constructs to explicitly flag failures to the monitor, which unlike deadlocks and livelocks in conventional process algebras, propagate globally and aborts the whole system’s execution. Although \(\text {CSP}_E\) has a trace semantics along with an implementation demonstrating acceptable performance, it lacks an operational semantics. An operational semantics is not only more accessible than trace semantics but also indispensable for ensuring the correctness of the implementation. Furthermore, a process algebra like \(\text {CSP}_E\) admits multiple denotational semantics appropriate for different purposes, and an operational semantics is the basis for justifying such semantics’ integrity and relevance. In this paper, we develop an SOS-style operational semantics for \(\text {CSP}_E\), which properly accounts for explicit failures and will serve as a basis for further study of its properties, its optimization, and its use in runtime verification.

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

References

  1. Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473–481. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_31

    Chapter  Google Scholar 

  2. Bloom, B.: Structural operational semantics for weak bisimulations. Theoret. Comput. Sci. 146(1), 25–68 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  4. Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR 2017) (2017, to appear)

    Google Scholar 

  5. van Glabbeek, R.J.: The linear time - branching time spectrum I. In: The Semantics of Concrete, Sequential Processes, Chap. 1, pp. 3–100. Elsevier (2001)

    Google Scholar 

  6. Groote, J.F.: Transition system specifications with negative premises. Theoret. Comput. Sci. 118(2), 263–299 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  7. Havelund, K., Reger, G.: Specification of parametric monitors. In: Drechsler, R., Kühne, U. (eds.) Formal Modeling and Verification of Cyber-Physical Systems, pp. 151–189. Springer, Wiesbaden (2015). doi:10.1007/978-3-658-09994-7_6

    Chapter  Google Scholar 

  8. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)

    MATH  Google Scholar 

  9. Mitchell, J.C.: Foundations for Programming Languages. MIT Press, New York (1996)

    Google Scholar 

  10. Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60, 17–139 (2004)

    MathSciNet  MATH  Google Scholar 

  11. Roscoe, A.: The expressiveness of CSP with priority. Electron. Notes Theor. Comput. Sci. 319, 387–401 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  12. Yamagata, Y., Artho, C., Hagiya, M., Inoue, J., Ma, L., Tanabe, Y., Yamamoto, M.: Runtime monitoring for concurrent systems. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 386–403. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_24

    Chapter  Google Scholar 

Download references

Acknowledgment

The authors would like to thank Yoshinao Isobe and Adrian Francalanza for comments on an earlier draft of this paper and stimulating discussions.

Author information

Authors and Affiliations

  1. National Institute of Advanced Industrial Science and Technology (AIST), 1-8-31 Midorigaoka, Ikeda, Osaka, 563-8577, Japan

    Jun Inoue & Yoriyuki Yamagata

Authors
  1. Jun Inoue
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yoriyuki Yamagata
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jun Inoue .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Inoue, J., Yamagata, Y. (2017). Operational Semantics of Process Monitors. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation