Monitoring with Parametrized Extended Life Sequence Charts

• Autorzy: Chai M. , Schlingloff B. -H.

Identyfikatory

DOI

10.3233/FI-2017-1536

• Języki publikacji: EN

Abstrakty

EN

Runtime verification is a lightweight formal method that checks whether an execution of a system satisfies a given property. A challenge in building a runtime verification system is to define a suitable monitoring specification language, i.e., a language that is expressive, of reasonable complexity, and easy to understand. In this paper, we extend live sequence charts (LSCs, [1]) for the specification of properties in systems monitoring. We define Parametrized extended LSCs (PeLSCs) by introducing the notions of necessary prechart, concatenation, and conditionand assignment-structure. With these PeLSCs, necessary and sufficient conditions of certain observations, and parametric properties can be specified in an intuitive way. We prove some results about the expressiveness of extended LSCs. In particular, we show that LSCs with necessary precharts are strictly more expressive than standard LSCs, and that iteration-free extended LSCs have the same expressive power as linear temporal logic (LTL). To generate monitors, we develop translations of PeLSCs into hybrid logic. We show that the complexity of the word problem of PeLSCs is linear with respect to the length of input traces, thus our formalism is well-suited for online monitoring of communicating systems.

Słowa kluczowe

EN

hybrid logic; live sequence charts; LTL; parameterized property; runtime verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 153, nr 3
• Strony: 173--198
• Opis fizyczny: Bibliogr. 42 poz., rys., wykr.

Twórcy

autor

Chai M.

• National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, China
• Institut für Informatik, Humboldt Universität zu Berlin, Germany

autor

Schlingloff B. -H.

• Institut für Informatik, Humboldt Universität zu Berlin, Germany
• Fraunhofer FOKUS, Berlin, Germany

Bibliografia

• [1] Damm W, Harel D. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 2001;19(1):45–80. doi:10.1023/A:1011227529550.
• [2] Havelund K. Monitoring with Data Automata. In: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, pp. 254–273. Springer, 2014. doi:10.1007/978-3-662-45231-8_18.
• [3] Ben-abdallah H, Leue S. Timing Constraints in Message Sequence Chart Specifications. In: In IFIP. Chapman. Hall, 1997. doi:10.1007/978-0-387-35271-8_6.
• [4] Chai M, Schlingloff BH. Monitoring Systems with Extended Live Sequence Charts. In: Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings. 2014 pp. 48–63. doi:10.1007/978-3-319-11164-3_5. URL http://dx.doi.org/10.1007/978-3-319-11164-3\_5.
• [5] Chai M, Schlingloff BH. Monitoring with Parametrized Extended Life Sequence Charts. In: Concurrency, Specification & Programming. 2015 pp. 88–102.
• [6] Blackburn P, Seligman J. Hybrid Languages. Journal of Logic, Language and Information, 1995;4(3):251–272. doi:10.1007/BF01049415. URL http://dx.doi.org/10.1007/BF01049415.
• [7] Alur R, Yannakakis M. Model Checking of Message Sequence Charts. In: CONCUR’ 99 Concurrency Theory, pp. 114–129. Springer, 1999. doi:10.1007/3-540-48320-9_10.
• [8] Simmonds J, Chechik M, Nejati S, Litani E, O’Farrell B. Property Patterns for Runtime Monitoring of Web Service Conversations. In: Runtime Verification. Springer, 2008 pp. 137–157. doi:10.1007/978-3-540-89247-2 9.
• [9] Ciraci S, Malakuti S, Katz S, Aksit M. Checking the Correspondence between UML Models and Implementation. In: Runtime Verification. Springer, 2010 pp. 198–213. URL http://doc.utwente.nl/74133/.
• [10] Harel D, Kugler H, Marelly R, Pnueli A. Smart Play-out of Behavioral Requirements. In: Formal Methods in Computer-aided Design. Springer, 2002 pp. 378–398. doi:10.1007/3-540-36126-X_23.
• [11] Bontemps Y, Schobbens PY. The Computational Complexity of Scenario-based Agent Verification and Design. Journal of Applied Logic, 2007;5(2):252–276. URL https://doi.org/10.1016/j.jal.2005.12.013.
• [12] Kugler H, Harel D, Pnueli A, Lu Y, Bontemps Y. Temporal Logic for Scenario-based Specifications. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 445–460. Springer, 2005. doi:10.1007/978-3-540-31980-1_29.
• [13] Harel D, Maoz S, Segall I. Some Results on the Expressive Power and Complexity of LSCs. In: Pillars of computer science, pp. 351–366. Springer, 2008. doi:10.1007/978-3-540-78127-1_19.
• [14] Kumar R, Mercer EG. Verifying Communication Protocols Using Live Sequence Chart Specifications. Electronic Notes in Theoretical Computer Science, 2009;250(2):33–48. URL https://doi.org/10.1016/j.entcs.2009.08.016.
• [15] Harel D, Marelly R. Playing with Time: On the Specification and Execution of Time-enriched LSCs. In: Modeling, Analysis and Simulation of Computer and Telecommunications Systems, 2002. MASCOTS 2002. Proceedings. 10th IEEE International Symposium on. IEEE, 2002 pp. 193–202. URL http://dl.acm.org/citation.cfm?id=882460.882611.
• [16] Barringer H, Goldberg A, Havelund K, Sen K. Rule-based Runtime Verification. In: Verification, Model Checking, and Abstract Interpretation. Springer, 2004 pp. 44–57. doi:10.1007/978-3-540-24622-0_5.
• [17] Barringer H, Rydeheard D, Havelund K. Rule Systems for Run-time Monitoring: from Eagle to RuleR. Journal of Logic and Computation, 2010;20(3):675–706. URL https://doi.org/10.1093/logcom/exn076.
• [18] Barringer H, Fisher M, Gabbay D, Gough G, Owens R. MetateM: A Framework for Programming in Temporal Logic. In: de Bakker J, de Roever WP, Rozenberg G (eds.), Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pp. 94–129. Springer Berlin Heidelberg. ISBN 978-3-540-52559-2, 1990. doi:10.1007/3-540-52559-9_62. URL http://dx.doi.org/10.1007/3-540-52559-9_62.
• [19] Forgy CL. Rete: A Fast Algorithm for the Many Pattern/many Object Pattern Match Problem. Artificial intelligence, 1982;19(1):17–37.
• [20] Havelund K. Rule-based Runtime Verification Revisited. International Journal on Software Tools for Technology Transfer, 2015;17(2):143–170. doi:10.1007/s10009-014-0309-2.
• [21] Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták O, De Moor O, Sereni D, Sittampalam G, Tibble J. Adding Trace Matching with Free Variables to AspectJ. In: ACM SIGPLAN Notices, volume 40. ACM, 2005 pp. 345–364.
• [22] Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold WG. An Overview of AspectJ. In: ECOOP 2001Object-Oriented Programming, pp. 327–354. Springer, 2001. ISBN:3-540-42206-4.
• [23] Barringer H, Havelund K. Trace Contract: A Scala DSL for Trace Analysis. In: Butler M, Schulte W (eds.), FM 2011: Formal Methods, volume 6664 of Lecture Notes in Computer Science, pp. 57–72. Springer Berlin Heidelberg. ISBN 978-3-642-21436-3, 2011. doi:10.1007/978-3-642-21437-0 7. URL http://dx.doi.org/10.1007/978-3-642-21437-0_7.
• [24] Chen F, Roşu G. Mop: an Efficient and Generic Runtime Verification Framework. In: ACM SIGPLAN Notices, volume 42. ACM, 2007 pp. 569–588. doi:10.1145/1297105.1297069.
• [25] Meredith PO, Jin D, Griffith D, Chen F, Roşu G. An Overview of the MOP Runtime Verification Framework. International Journal on Software Tools for Technology Transfer, 2012;14(3):249–289. doi:10.1007/s10009-011-0198-6.
• [26] Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard D. Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In: FM 2012: Formal Methods, pp. 68–84. Springer, 2012. doi:10.1007/978-3-642-32759-9_9.
• [27] Bauer A, Leucker M, Schallhart C. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM), 2011;20(4):14. doi:10.1145/2000799.2000800.
• [28] Basin D, Klaedtke F, Zălinescu E. Algorithms for Monitoring Real-time Properties. In: Runtime Verification. Springer, 2012 pp. 260–275. doi:10.1007/978-3-642-29860-8_20.
• [29] Chai M, Schlingloff BH. A Rewriting Based Monitoring Algorithm for TPTL. In: Concurrency, Specification & Programming. 2013 pp. 61–72.
• [30] Stolz V. Temporal Assertions with Parametrized Propositions. Journal of Logic and Computation, 2010;20(3):743–757. doi:10.1093/logcom/exn078.
• [31] Merz S. Decidability and Incompleteness Results for First-order Temporal Logics of Linear Time. Journal of Applied Non-Classical Logics, 1992;2(2):139–156.
• [32] Bauer A, Küster JC, Vegliach G. From Propositional to First-order Monitoring. In: Runtime Verification. Springer, 2013 pp. 59–75.
• [33] Halle S, Villemaire R. Runtime Monitoring of Message-based Workflows with Data. In: Enterprise Distributed Object Computing Conference, 2008. EDOC’08. 12th International IEEE. IEEE, 2008 pp. 63–72. doi:10. 1109/EDOC.2008.32.
• [34] Basin D, Klaedtke F, Müller S. Policy Monitoring in First-order Temporal Logic. In: Computer Aided Verification. Springer, 2010 pp. 1–18. doi:10.1007/978-3-642-14295-6_1.
• [35] Basin D, Caronni G, Ereth S, Harvan M, Klaedtke F, Mantel H. Scalable Offline Monitoring. In: Bonakdarpour B, Smolka S (eds.), Runtime Verification, volume 8734 of Lecture Notes in Computer Science, pp. 31–47. Springer International Publishing. ISBN 978-3-319-11163-6, 2014. doi:10.1007/978-3-319-11164-3_4. URL http://dx.doi.org/10.1007/978-3-319-11164-3_4.
• [36] 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.
• [37] 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, 2008;7(2):157–175. doi:10.1007/s10270-007-0069-5.
• [38] Fisher J, Harel D, Hubbard EJA, Piterman N, Stern MJ, Swerdlin N. Combining State-based and Scenariobased Approaches in Modeling Biological Systems. In: Computational Methods in Systems Biology. Springer, 2005 pp. 236–241.
• [39] Alur R, Etessami K, Yannakakis M. Inference of Message Sequence Charts. Software Engineering, IEEE Transactions on, 2003;29(7):623–633. doi:10.1109/TSE.2003.1214326.
• [40] Bontemps Y. Relating Inter-Agent and Intra-Agent Specifications. Ph.D. thesis, PhD thesis, University of Namur (Belgium), 2005.
• [41] Franceschet M, de Rijke M, Schlingloff BH. Hybrid Logics on Linear Structures: Expressivity and Complexity. In: Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings. 10th International Symposium on. IEEE, 2003 pp. 166–173. doi:10.1109/TIME.2003.1214893.
• [42] Ölveczky PC. Real-Time Maude 2.3 Manual. Research report http://urn.nb.no/URN: NBN: no-35645, 2004. URL http://urn.nb.no/URN:NBN:no-18692Delav.