Advertisement

Runtime Monitoring of Stream Logic Formulae

  • Sylvain HalléEmail author
  • Raphaël Khoury
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9482)

Abstract

We introduce a formal notation for the processing of event traces called Stream Logic (SL). A monitor evaluates a Boolean condition over an input trace, while a filter outputs events from an input trace depending on some monitor’s verdict; both constructs can be freely composed. We show how all operators of Linear Temporal Logic, as well as the parametric slicing of an input trace, can be written as Stream Logic constructs.

Keywords

Formal Semantic Linear Temporal Logic Formal Notation Linear Temporal Logic Formula Output Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Barre, B., Klein, M., Soucy-Boivin, M., Ollivier, P.-A., Hallé, S.: MapReduce for parallel trace validation of LTL properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 184–198. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-35632-2_20 CrossRefGoogle Scholar
  2. 2.
    Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  3. 3.
    Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from eagle to RuleR. J. Logic Comput. 20(3), 675–706 (2010)CrossRefMathSciNetzbMATHGoogle Scholar
  4. 4.
    Basin, D., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Groce, A., Havelund, K., Smith, M.H.: From scripts to specifications: the evolution of a flight software testing effort. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) ICSE (2), pp. 129–138. ACM (2010)Google Scholar
  6. 6.
    Hallé, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192–206 (2012)CrossRefGoogle Scholar
  7. 7.
    Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012). doi: 10.1007/s10009-011-0198-6 CrossRefGoogle Scholar
  8. 8.
    Verbeek, H.M.W., Buijs, J.C.A.M., van Dongen, B.F., van der Aalst, W.M.P.: XES, XESame, and ProM 6. In: Soffer, P., Proper, E. (eds.) CAiSE Forum 2010. LNBIP, vol. 72, pp. 60–75. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Laboratoire d’informatique formelleUniversité du Québec à ChicoutimiChicoutimiCanada

Personalised recommendations