nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Industrial Experiences with Runtime Verification of Financial Transaction Systems: Lessons Learnt and Standing Challenges

verfasst von : Christian Colombo, Gordon J. Pace

Erschienen in: Lectures on Runtime Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The chapter will focus on experiences the authors had in applying runtime verification in industrial settings, in particular on financial transaction systems. We discuss how runtime verification can be introduced in the software development lifecycle and who are the people to be involved and when. Furthermore, we investigate what kind of properties have been found useful in practise and how these were monitored to keep intrusion to a minimum. Next, we describe two significant case studies which have been successfully carried out in the past, and conclude by outlining a number of challenges which we believe still need to be addressed for runtime verification to become more mainstream in industrial settings.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Runtime Verification for Decentralised and Distributed Systems

Due to non-disclosure agreements, one of the companies cannot be named. However, it is worth noting that both companies had a R&D team of 50–100 persons.

https://www.um.edu.mt/ict/cs/research/projects/gomta.

https://www.openpaymentsecosystem.eu.

Other than software events, one may for example capture the state of the hardware, or perform regular sampling of the variables. However, in this chapter we focus on the more commonly used software events.

Users all had an undergraduate degree which covered automata and they did not have full formal training in using formal logics such as LTL, they were comfortable using automata.

Abela, P., Colombo, C., Pace, G.J.: Offline runtime verification with real-time properties: a case study. In: University of Malta Workshop in ICT (WICT 2009) (2009)

Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005). https://doi.org/10.1016/j.tcs.2004.11.007 MathSciNetCrossRefMATH

Artho, C., Biere, A.: Combined static and dynamic analysis. Electr. Notes Theor. Comput. Sci. 131, 3–14 (2005). https://doi.org/10.1016/j.entcs.2005.01.018 CrossRef

Azzopardi, S., Colombo, C., Pace, G.: A model-based approach to combining static and dynamic verification techniques. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 416–430. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_29 CrossRef

Azzopardi, S., Colombo, C., Pace, G.J., Vella, B.: Compliance checking in the open payments ecosystem. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 337–343. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_23

Baresi, L., Ghezzi, C.: The disappearing boundary between development-time and run-time. In: Proceedings of the FSE/SDP Workshop on Future of Software Engineering Research, FoSER 2010, pp. 17–22. ACM, New York (2010). http://doi.acm.org/10.1145/1882362.1882367

Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168–182. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_18 CrossRef

Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: 27th IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2013, Cambridge, MA, USA, 20–24 May 2013 (2013). https://doi.org/10.1109/IPDPS.2013.105

Bodden, E., Hendren, L., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative runtime verification with tracematches. J. Log. Comput. 20(3), 707–723 (2010). https://doi.org/10.1093/logcom/exn077 MathSciNetCrossRefMATH

10.

Bodden, E., Hendren, L., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 525–549. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73589-2_25 CrossRef

11.

Bodden, E., Lam, P., Hendren, L.: Clara: a framework for partially evaluating finite-state runtime monitors ahead of time. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 183–197. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_15 CrossRef

12.

Calafato, A., Colombo, C., Pace, G.J.: A controlled natural language for tax fraud detection. In: Davis, B., Pace, G.J.J., Wyner, A. (eds.) CNL 2016. LNCS (LNAI), vol. 9767, pp. 1–12. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41498-0_1 CrossRef

13.

Cauchi, A., Colombo, C., Francalanza, A., Micallef, M., Pace, G.J.: Using gherkin to extract tests and monitors for safer medical device interaction design. In: Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2016, Brussels, Belgium, 21–24 June 2016, pp. 275–280. ACM, New York (2016). http://doi.acm.org/10.1145/2933242.2935868

14.

Centonze, P., Flynn, R.J., Pistoia, M.: Combining static and dynamic analysis for automatic identification of precise access-control policies. In: 23rd Annual Computer Security Applications Conference (ACSAC 2007), Miami Beach, Florida, USA, 10–14 December 2007, pp. 292–303 (2007). https://doi.org/10.1109/ACSAC.2007.14

15.

Chimento, J.M., Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 297–305. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_21 CrossRef

16.

Chircop, L., Colombo, C., Micallef, M.: Exploring the link between automatic specification inference and test suite quality (2017). Submitted for publication

17.

Colombo, C., Dimech, G., Francalanza, A.: Investigating instrumentation techniques for ESB runtime verification. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 99–107. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_7 CrossRef

18.

Colombo, C., Francalanza, A., Gatt, R.: Elarva: a monitoring tool for erlang. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 370–374. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_29 CrossRef

19.

Colombo, C., Francalanza, A., Mizzi, R., Pace, G.J.: polyLarva: runtime verification with configurable resource-aware monitoring boundaries. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 218–232. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_15 CrossRef

20.

Colombo, C., Grech, J.-P., Pace, G.J.: A controlled natural language for business intelligence monitoring. In: Biemann, C., Handschuh, S., Freitas, A., Meziane, F., Métais, E. (eds.) NLDB 2015. LNCS, vol. 9103, pp. 300–306. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19581-0_27 CrossRef

21.

Colombo, C., Pace, G.J.: Fast-forward runtime monitoring — an industrial case study. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 214–228. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_22 CrossRef

22.

Colombo, C., Pace, G.J., Abela, P.: Compensation-aware runtime monitoring. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 214–228. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_17 CrossRef

23.

Colombo, C., Pace, G.J., Abela, P.: Safer asynchronous runtime monitoring using compensations. Formal Methods Syst. Des. 41(3), 269–294 (2012). https://doi.org/10.1007/s10703-012-0142-8 CrossRefMATH

24.

Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135–149. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03240-0_13 CrossRef

25.

Colombo, C., Pace, G.J., Schneider, G.: LARVA – safer monitoring of real-time Java programs (tool paper). In: Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23–27 November 2009, pp. 33–37 (2009). https://doi.org/10.1109/SEFM.2009.13

26.

Falzon, K., Pace, G.J.: Combining testing and runtime verification techniques. In: Machado, R.J., Maciel, R.S.P., Rubin, J., Botterweck, G. (eds.) MOMPES 2012. LNCS, vol. 7706, pp. 38–57. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38209-3_3 CrossRef

27.

Giannakopoulou, D., Pasareanu, C.S., Lowry, M., Washington, R.: Lifecycle verification of the NASA ames K9 rover executive. Technical report, NASA (2004). http://ti.arc.nasa.gov/publications

28.

Hoare, C.: Programming is an engineering profession. In: Wallis, P. (ed.) State of the Art Report 11, No. 3: Software Engineering, pp. 77–84. Pergamon/Infotech (1983). Also Oxford PRG Monograph No. 27; and IEEE Softw. 1(2)

29.

Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24 CrossRef

30.

Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Nickovic, D.: From signal temporal logic to FPGA monitors. In: 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, 21–23 September 2015, pp. 218–227 (2015). https://doi.org/10.1109/MEMCOD.2015.7340489

31.

Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0053381

32.

Kuhn, T.: A survey and classification of controlled natural languages. CoRR abs/1507.01701 (2015). http://arxiv.org/abs/1507.01701

33.

Medhat, R., Bonakdarpour, B., Fischmeister, S., Joshi, Y.: Accelerated runtime verification of LTL specifications with counting semantics. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 251–267. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_16 CrossRef

34.

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, pp. 46–57 (1977). https://doi.org/10.1109/SFCS.1977.32

35.

Smaragdakis, Y., Csallner, C.: Combining static and dynamic reasoning for bug detection. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 1–16. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73770-4_1 CrossRef

36.

Tamura, G., et al.: Towards practical runtime verification and validation of self-adaptive software systems. In: de Lemos, R., Giese, H., Müller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 108–132. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35813-5_5 CrossRef

37.

Wonisch, D., Schremmer, A., Wehrheim, H.: Zero overhead runtime monitoring. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 244–258. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40561-7_17 CrossRef

Titel: Industrial Experiences with Runtime Verification of Financial Transaction Systems: Lessons Learnt and Standing Challenges
verfasst von: Christian Colombo
Gordon J. Pace
Verlag: Springer International Publishing
Buch: Lectures on Runtime Verification
Print ISBN: 978-3-319-75631-8

Electronic ISBN: 978-3-319-75632-5

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-75632-5_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner