Skip to main content
SpringerLink
Log in

Monitoring Systems with Extended Live Sequence Charts

  • Conference paper
Book cover Runtime Verification (RV 2014)

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

Included in the following conference series:

Abstract

A problem with most runtime verification techniques is that the monitoring specification formalisms are often complex. In this paper, we propose an extension of live sequence charts (LSCs) which avoids this problem. We extend the standard LSCs as proposed by Damm and Harel by introducing the notion of “sufficient prechart”, and by adding concatenation and iteration of charts. With these extended LSCs, necessary and sufficient conditions of certain statements can be intuitively specified. Moreover, similar as for message sequence charts, sequencing and iteration allow to express multiple scenarios. We give a translation of extended LSCs into linear temporal logic formulae, and develop online monitoring algorithms for traces with respect to extended LSCs. We use our algorithm to test a concrete example from the European Train Control System (ETCS) standard, and evaluate it on several benchmarks. The results show the feasibility of our approach.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Yannakakis, M.: Model Checking of Message Sequence Charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Bauer, A., Küster, J.-C., Vegliach, G.: From Propositional to First-order Monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  3. Ben-abdallah, H., Leue, S.: Timing Constraints in Message Sequence Chart Specifications. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP, pp. 91–106. Springer, Boston (1997)

    Google Scholar 

  4. Bohn, J., Damm, W., Klose, J., Moik, A., Wittke, H., Ehrig, H., Kramer, B., Ertas, A.: Modeling and Validating Train System Applications Using Statemate and Live Sequence Charts. In: Proc. IDPT. Citeseer (2002)

    Google Scholar 

  5. Bontemps, Y.: Relating Inter-Agent and Intra-Agent Specifications. PhD thesis, PhD thesis, University of Namur, Belgium (2005)

    Google Scholar 

  6. Bontemps, Y., Schobbens, P.-Y.: The Computational Complexity of Scenario-based Agent Verification and Design. Journal of Applied Logic 5(2), 252–276 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  7. Chai, M., Schlingloff, H.: A Rewriting Based Monitoring Algorithm for TPTL. In: CS&P 2013, pp. 61–72. Citeseer (2013)

    Google Scholar 

  8. Chen, F., Roşu, G.: Java-MOP: A Monitoring Oriented Programming Environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Ciraci, S., Malakuti, S., Katz, S., Aksit, M.: Checking the Correspondence between UML Models and Implementation. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 198–213. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (version 2.6). University of Illinois, Urbana-Champaign 1(3), 4–6 (2011)

    Google Scholar 

  11. Combes, P., Harel, D., Kugler, H.: Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-engine Tool. Software & Systems Modeling 7(2), 157–175 (2008)

    Article  Google Scholar 

  12. Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1), 45–80 (2001)

    Article  MATH  Google Scholar 

  13. Fisher, J., Harel, D., Hubbard, E.J.A., Piterman, N., Stern, M.J., Swerdlin, N.: Combining State-based and Scenario-based Approaches in Modeling Biological Systems. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 236–241. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-out of Behavioral Requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Harel, D., Maoz, S.: Assert and Negate Revisited: Modal Semantics for UML Sequence Diagrams. Software & Systems Modeling 7(2), 237–252 (2008)

    Article  Google Scholar 

  16. Harel, D., Maoz, S., Segall, I.: Some Results on the Expressive Power and Complexity of LSCs. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Trakhtenbrot/Festschrift. LNCS, vol. 4800, pp. 351–366. Springer, Heidelberg (2008)

    Google Scholar 

  17. Havelund, K., Roşu, G.: Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science 55(2), 200–217 (2001)

    Article  Google Scholar 

  18. Kugler, H.-J., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal Logic for Scenario-based Specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Kumar, R., Mercer, E.G.: Verifying Communication Protocols Using Live Sequence Chart Specifications. Electronic Notes in Theoretical Computer Science 250(2), 33–48 (2009)

    Article  Google Scholar 

  20. Leucker, M., Schallhart, C.: A Brief Account of Runtime Verification. The Journal of Logic and Algebraic Programming 78(5), 293–303 (2009)

    Article  MATH  Google Scholar 

  21. Meredith, P.O., Jin, D., Chen, F., Roşu, G.: Efficient Monitoring of Parametric Context-free Patterns. Automated Software Engineering 17(2), 149–180 (2010)

    Article  Google Scholar 

  22. Roşu, G., Havelund, K.: Rewriting-based Techniques for Runtime Verification. Automated Software Engineering 12(2), 151–197 (2005)

    Article  Google Scholar 

  23. Simmonds, J., Chechik, M., Nejati, S., Litani, E., O’Farrell, B.: Property Patterns for Runtime Monitoring of Web Service Conversations. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 137–157. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Thati, P., Roşu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. Electronic Notes in Theoretical Computer Science 113, 145–162 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Humboldt Universität zu Berlin, Germany

    Ming Chai & Bernd-Holger Schlingloff

  2. Fraunhofer FOKUS, Germany

    Bernd-Holger Schlingloff

Authors
  1. Ming Chai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd-Holger Schlingloff
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4L7, Hamilton, ON, Canada

    Borzoo Bonakdarpour

  2. Department of Computer Science, State University of New York at Stony Brook, 1423 Computer Science, 11794-4400, Stony Brook, NY, USA

    Scott A. Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Chai, M., Schlingloff, BH. (2014). Monitoring Systems with Extended Live Sequence Charts. In: Bonakdarpour, B., Smolka, S.A. (eds) Runtime Verification. RV 2014. Lecture Notes in Computer Science, vol 8734. Springer, Cham. https://doi.org/10.1007/978-3-319-11164-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11164-3_5

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11163-6

  • Online ISBN: 978-3-319-11164-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation