nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Runtime Failure Prevention and Reaction

verfasst von : Yliès Falcone, Leonardo Mariani, Antoine Rollet, Saikat Saha

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

This chapter describes how to use in-the-field runtime techniques to improve the dependability of software systems. In particular, we first present an overall vision of the problem of ensuring highly-dependable behaviours at runtime based on the concept of autonomic monitor, and then we present the two families of relevant approaches for this purpose. First, we present techniques related to runtime enforcement that can prevent the system producing bad behaviours. Second, we describe healing techniques that can detect if the system has produced a bad behaviour and react to the situation accordingly (e.g., moving the system back to a correct state).

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 Monitoring Events that Carry Data

Nächstes Kapitel Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications

We follow the terminology of [40] which generalises previous terminologies used in runtime enforcement. We use the term enforcement mechanism to encompass definitions of mechanisms dedicated to enforcement described at different abstraction levels. Moreover, using the term enforcement mechanism allows us to abstract away the architecture of the autonomic monitor and its placement w.r.t. the monitored system.

This is the notion of transparency adopted in a majority of papers on runtime enforcement. Some research efforts notice that this notion of transparency only constrains correct execution sequences; and they advocate that constraints should be placed on how an enforcement mechanism transforms incorrect execution sequences [11, 12, 58].

We note that some ongoing research efforts study hyper-properties [26], which resemble policies. We also note ongoing work advocating monitoring hyper-properties [16].

As was the case in runtime verification, early work on runtime enforcement considered infinite executions.

Hamlen et al. [50] additionally introduce the notion of RW-enforceable policies (policies enforceable by enforcement mechanisms with Program Rewriting abilities), and use it to define a more precise characterisation of enforceable security policies. They model the untrusted programs as Türing machines with deterministic transition relations with three infinite-length tapes. They divide enforcement mechanisms into three categories: static analysers, reference monitors, and program rewriters. Static analysers operate strictly prior to running the untrusted program. Reference monitors intercept events or actions the program under scrutiny and intervene before occurrence of an event violating the policy, by terminating it or applying some other corrective action. Program rewriters modify in a finite time the program under scrutiny prior to execution.

Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., Traon, Y.L., Octeau, D., McDaniel, P.D.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, UK, 9–11 June 2014, pp. 259–269. ACM (2014)

Avizienis, A.: The N-version approach to fault-tolerant software. IEEE Trans. Softw. Eng. (TSE) 11(12), 1491–1501 (1985)CrossRef

Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Shin, Y.: The Oracle problem in software testing: a survey. IEEE Trans. Softw. Eng. (TSE) 41(5), 507–525 (2015)CrossRef

Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. 1–40 (2017). https://doi.org/10.1007/s10009-017-0454-5

Basin, D., Jugé, V., Klaedtke, F., Zălinescu, E.: Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur. 16(1), 3:1–3:26 (2013). http://doi.acm.org/10.1145/2487222.2487225 CrossRefMATH

Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)CrossRef

Bauer, A., Falcone, Y.: Decentralised LTL monitoring. Formal Meth. Syst. Des. 48(1–2), 46–93 (2016)CrossRefMATH

Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Proceedings of the Workshop on Foundations of Computer Security (FCS 2002), Copenhagen, Denmark (2002)

Bauer, L., Ligatti, J., Walker, D.: Composing security policies with polymer. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, 12–15 June 2005, pp. 305–314. ACM (2005)

10.

Beauquier, D., Cohen, J., Lanotte, R.: Security policies enforcement using finite and pushdown edit automata. Int. J. Inf. Sec. 12(4), 319–336 (2013). https://doi.org/10.1007/s10207-013-0195-8 CrossRefMATH

11.

Bielova, N., Massacci, F.: Do you really mean what you actually enforced? - edited automata revisited. Int. J. Inf. Sec. 10(4), 239–254 (2011)CrossRef

12.

Bielova, N., Massacci, F.: Predictability of enforcement. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 73–86. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19125-1_6 CrossRef

13.

Bielova, N., Massacci, F.: Iterative enforcement by suppression: towards practical enforcement theories. J. Comput. Secur. 20(1), 51–79 (2012)CrossRef

14.

Blech, J.O., Falcone, Y., Becker, K.: Towards certified runtime verification. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 494–509. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_34 CrossRef

15.

Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: - runtime enforcement for reactive systems. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, 11–18 April 2015, Proceedings, pp. 533–548 (2015)

16.

Bonakdarpour, B., Finkbeiner, B.: Runtime verification for HyperLTL. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 41–45. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_4 CrossRef

17.

Bultan, T., Sen, K. (eds.): Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, 10–14 July 2017. ACM (2017)

18.

Carzaniga, A., Gorla, A., Mattavelli, A., Perino, N., Pezzè, M.: Automatic recovery from runtime failures. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 782–791. IEEE Press (2013)

19.

Carzaniga, A., Gorla, A., Perino, N., Pezzè, M.: Automatic workarounds: exploiting the intrinsic redundancy of web applications. ACM Trans. Softw. Eng. Methodol. (TOSEM) 24(3), 16 (2015)CrossRef

20.

Chabot, H., Khoury, R., Tawbi, N.: Generating in-line monitors for Rabin automata. In: Jøsang, A., Maseng, T., Knapskog, S.J. (eds.) NordSec 2009. LNCS, vol. 5838, pp. 287–301. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04766-4_20 CrossRef

21.

Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. Technical report, Stanford University, Department of Computer Science (1992)

22.

Chang, H., Mariani, L., Pezzè, M.: In-field healing of integration problems with COTS components. In: Proceedings of the International Conference on Software Engineering (ICSE) (2009)

23.

Chang, H., Mariani, L., Pezzè, M.: Exception handlers for healing component-based systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 22(4), 30 (2013)CrossRef

24.

Charafeddine, H., El-Harake, K., Falcone, Y., Jaber, M.: Runtime enforcement for component-based systems. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, 13–17 April 2015, pp. 1789–1796. ACM (2015)

25.

Chen, F., d’Amorim, M., Roşu, G.: Checking and correcting behaviors of Java programs at runtime with Java-MOP. Electron. Notes Theor. Comput. Sci. 144(4), 3–20 (2006)CrossRef

26.

Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23–25 June 2008, pp. 51–65. IEEE Computer Society (2008)

27.

Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. Formal Meth. Syst. Des. 49(1–2), 109–158 (2016). https://doi.org/10.1007/s10703-016-0251-x CrossRef

28.

Cuppens, F., Cuppens-Boulahia, N., Ramard, T.: Availability enforcement by obligations and aspects identification. In: The First International Conference on Availability, Reliability and Security, ARES 2006, 10 pp. IEEE (2006)

29.

Ding, R., Fu, Q., Lou, J.G., Lin, Q., Zhang, D., Shen, J., Xie, T.: Healing online service systems via mining historical issue repositories. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 318–321. IEEE (2012)

30.

Dolzhenko, E., Ligatti, J., Reddy, S.: Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Secur. 14(1), 47–60 (2015)CrossRef

31.

El-Harake, K., Falcone, Y., Jerad, W., Langet, M., Mamlouk, M.: Blocking advertisements on android devices using monitoring techniques. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 239–253. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_17

32.

El-Hokayem, A., Falcone, Y.: Monitoring decentralized specifications. In: Bultan and Sen [17], pp. 125–135

33.

El-Hokayem, A., Falcone, Y.: THEMIS: a tool for decentralized monitoring algorithms. In: Bultan and Sen [17], pp. 372–375

34.

Erlingsson, Ú., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: Kienzle, D.M., Zurko, M.E., Greenwald, S.J., Serbau, C. (eds.) Proceedings of the 1999 Workshop on New Security Paradigms, Caledon Hills, ON, Canada, 22–24 September 1999, pp. 87–95. ACM (1999)

35.

Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 89–105. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_9 CrossRef

36.

Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for Android applications with RV-Droid. In: Qadeer and Tasiran [80], pp. 88–95

37.

Falcone, Y., Fernandez, J.-C., Mounier, L.: Synthesizing enforcement monitors wrt. the safety-progress classification of properties. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 41–55. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89862-7_3 CrossRef

38.

Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer 14(3), 349–382 (2012)CrossRef

39.

Falcone, Y., Jaber, M.: Fully automated runtime enforcement of component-based systems with formal and sound recovery. Int. J. Softw. Tools Technol. Transf. 19(3), 1–25 (2016)

40.

Falcone, Y., Jéron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2–41 (2016)

41.

Falcone, Y., Marchand, H.: Runtime enforcement of K-step opacity. In: Proceedings of the 52nd IEEE Conference on Decision and Control, CDC 2013, 10–13 December 2013, Firenze, Italy, pp. 7271–7278. IEEE (2013)

42.

Falcone, Y., Marchand, H.: Enforcement and validation (at runtime) of various notions of opacity. Discrete Event Dyn. Syst. 25(4), 531–570 (2015). http://dx.doi.org/10.1007/s10626-014-0196-4 MathSciNetCrossRefMATH

43.

Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Meth. Syst. Des. 38(3), 223–262 (2011)CrossRefMATH

44.

Fong, P.W.L.: Access control by tracking shallow execution history. In: 2004 IEEE Symposium on Security and Privacy (S&P 2004), 9–12 May 2004, Berkeley, CA, USA, pp. 43–55. IEEE Computer Society (2004)

45.

Goffi, A., Gorla, A., Mattavelli, A., Pezzè, M., Tonella, P.: Search-based synthesis of equivalent method sequences. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE) (2014)

46.

Goues, C.L., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. IEEE Trans. Softw. Eng. (TSE) 38(1), 54–72 (2012)CrossRef

47.

Hallé, S., Khoury, R., El-Hokayem, A., Falcone, Y.: Decentralized enforcement of artifact lifecycles. In: Matthes, F., Mendling, J., Rinderle-Ma, S. (eds.) 20th IEEE International Enterprise Distributed Object Computing Conference, EDOC 2016, Vienna, Austria, 5–9 September 2016, pp. 1–10. IEEE Computer Society (2016)

48.

Hallé, S., Khoury, R., Betti, Q., El-Hokayem, A., Falcone, Y.: Decentralized enforcement of document lifecycle constraints. Information Systems (2017)

49.

Hamlen, K.W., Morrisett, G., Schneider, F.B.: Certified in-lined reference monitoring on .net. In: Sreedhar, V.C., Zdancewic, S. (eds.) Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, PLAS 2006, Ottawa, Ontario, Canada, 10 June 2006, pp. 7–16. ACM (2006)

50.

Hamlen, K.W., Morrisett, G., Schneider, F.B.: Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. (TOPLAS) 28(1), 175–205 (2006)CrossRef

51.

Hosek, P., Cadar, C.: Safe software updates via multi-version execution. In: Proceedings of the International Conference on Software Engineering (ICSE) (2013)

52.

Humphrey, L., Könighofer, B., Könighofer, R., Topcu, U.: Synthesis of admissible shields. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 134–151. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49052-6_9 CrossRef

53.

IEEE: systems and software engineering - vocabulary. Technical report, ISO/IEC/IEEE 24765. IEEE International Standard (2010)

54.

Johansen, H.D., Birrell, E., van Renesse, R., Schneider, F.B., Stenhaug, M., Johansen, D.: Enforcing privacy policies with meta-code. In: Kono, K., Shinagawa, T. (eds.) Proceedings of the 6th Asia-Pacific Workshop on Systems, APSys 2015, Tokyo, Japan, 27–28 July 2015, pp. 16:1–16:7. ACM (2015)

55.

Jones, J.A., Harrold, M.J.: Empirical evaluation of the tarantula automatic fault-localization technique. In: Proceedings of the International Conference on Automated Software Engineering (ASE) (2005)

56.

Kephart, J.O., Chess, D.M.: The vision of autonomic computing. Computer 36(1), 41–50 (2003)MathSciNetCrossRef

57.

Khoury, R., Hallé, S.: Runtime enforcement with partial control. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds.) FPS 2015. LNCS, vol. 9482, pp. 102–116. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30303-1_7 CrossRef

58.

Khoury, R., Tawbi, N.: Corrective enforcement: a new paradigm of security policy enforcement by monitors. ACM Trans. Inf. Syst. Secur. 15(2), 10:1–10:27 (2012)CrossRef

59.

Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? A survey. Comput. Sci. Rev. 6(1), 27–45 (2012)CrossRefMATH

60.

Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Computational analysis of run-time monitoring - fundamentals of Java-MAC. Electr. Notes Theor. Comput. Sci. 70(4), 80–94 (2002)CrossRef

61.

Kumar, A., Ligatti, J., Tu, Y.-C.: Query monitoring and analysis for database privacy - a security automata model approach. In: Wang, J., Cellary, W., Wang, D., Wang, H., Chen, S.-C., Li, T., Zhang, Y. (eds.) WISE 2015. LNCS, vol. 9419, pp. 458–472. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26187-4_42 CrossRef

62.

Ligatti, J., Bauer, L., Walker, D.: Enforcing non-safety security policies with program monitors. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 355–373. Springer, Heidelberg (2005). https://doi.org/10.1007/11555827_21 CrossRef

63.

Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3), 19:1–19:41 (2009)CrossRef

64.

Ligatti, J., Reddy, S.: A theory of runtime enforcement, with results. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 87–100. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15497-3_6 CrossRef

65.

Martinelli, F., Matteucci, I.: Through modeling to synthesis of security automata. Electr. Notes Theor. Comput. Sci. 179, 31–46 (2007). http://dx.doi.org/10.1016/j.entcs.2006.08.029 CrossRef

66.

Martinelli, F., Matteucci, I., Mori, P., Saracino, A.: Enforcement of U-XACML history-based usage control policy. In: Barthe, G., Markatos, E., Samarati, P. (eds.) STM 2016. LNCS, vol. 9871, pp. 64–81. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46598-2_5 CrossRef

67.

Martinelli, F., Matteucci, I., Saracino, A., Sgandurra, D.: Remote policy enforcement for trusted application execution in mobile environments. In: Bloem, R., Lipp, P. (eds.) INTRUST 2013. LNCS, vol. 8292, pp. 70–84. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03491-1_5 CrossRef

68.

Martinelli, F., Matteucci, I., Saracino, A., Sgandurra, D.: Enforcing mobile application security through probabilistic contracts. In: Joosen, W., Martinelli, F., Heyman, T. (eds.) Proceedings of the 2014 ESSoS Doctoral Symposium Co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2014), Munich, Germany, 26 February 2014. CEUR Workshop Proceedings, vol. 1298. CEUR-WS.org (2014)

69.

Martinelli, F., Mori, P., Saracino, A.: Enhancing android permission through usage control: a BYOD use-case. In: Ossowski [70], pp. 2049–2056

70.

Ossowski, S. (ed.): Proceedings of the 31st Annual ACM Symposium on Applied Computing, Pisa, Italy, 4–8 April 2016. ACM (2016)

71.

Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)CrossRefMATH

72.

Pavlich-Mariscal, J., Michel, L., Demurjian, S.: A formal enforcement framework for role-based access control using aspect-oriented programming. In: Briand, L., Williams, C. (eds.) MODELS 2005. LNCS, vol. 3713, pp. 537–552. Springer, Heidelberg (2005). https://doi.org/10.1007/11557432_41 CrossRef

73.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H.: Runtime enforcement of parametric timed properties with practical applications. In: Lesage, J., Faure, J., Cury, J.E.R., Lennartson, B. (eds.) 12th International Workshop on Discrete Event Systems, WODES 2014, Cachan, France, 14–16 May 2014, pp. 420–427. International Federation of Automatic Control (2014)

74.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H.: Runtime enforcement of regular timed properties. In: Cho, Y., Shin, S.Y., Kim, S., Hung, C., Hong, J. (eds.) Symposium on Applied Computing, SAC 2014, Gyeongju, Republic of Korea, 24–28 March 2014, pp. 1279–1286. ACM (2014)

75.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H.: TiPEX: a tool chain for timed property enforcement during execution. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 306–320. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_22 CrossRef

76.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena-Timo, O.: Runtime enforcement of timed properties revisited. Formal Meth. Syst. Des. 45(3), 381–422 (2014)CrossRefMATH

77.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena-Timo, O.L.: Runtime enforcement of timed properties. In: Qadeer and Tasiran [80], pp. 229–244

78.

Pinisetty, S., Preoteasa, V., Tripakis, S., Jéron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. In: Ossowski [70], pp. 1628–1633

79.

Pinisetty, S., Preoteasa, V., Tripakis, S., Jéron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. Formal Meth. Syst. Des. 51(1), 1–46 (2017)CrossRefMATH

80.

Qadeer, S., Tasiran, S. (eds.): RV 2012. LNCS, vol. 7687. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2

81.

Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRefMATH

82.

Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)CrossRefMATH

83.

Renard, M.: GREP (2017). https://github.com/matthieurenard/GREP

84.

Renard, M., Falcone, Y., Rollet, A., Jéron, T., Marchand, H.: Optimal enforcement of (timed) properties with uncontrollable events. In: Mathematical Structures in Computer Science, pp. 1–46 (2017)

85.

Renard, M., Falcone, Y., Rollet, A., Pinisetty, S., Jéron, T., Marchand, H.: Enforcement of (timed) properties with uncontrollable events. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 542–560. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_31 CrossRef

86.

Renard, M., Rollet, A., Falcone, Y.: Runtime enforcement using Büchi games. In: Proceedings of Model Checking Software - 24th International Symposium, SPIN 2017, Co-located with ISSTA 2017, Santa Barbara, USA, pp. 70–79. ACM, July 2017

87.

Riganelli, O., Micucci, D., Mariani, L., Falcone, Y.: Verifying policy enforcers. In: Proceedings of the International Conference on Runtime Verification (RV) (2017)

88.

Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)CrossRef

89.

Sridhar, M., Hamlen, K.W.: Flexible in-lined reference monitor certification: challenges and future directions. In: Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification, PLPV 2011, pp. 55–60 (2011)

90.

Swanson, J., Cohen, M.B., Dwyer, M.B., Garvin, B.J., Firestone, J.: Beyond the rainbow: self-adaptive failure avoidance in configurable systems. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE) (2014)

91.

Talhi, C., Tawbi, N., Debbabi, M.: Execution monitoring enforcement under memory-limitation constraints. Inf. Comput. 206(2–4), 158–184 (2008). https://doi.org/10.1016/j.ic.2007.07.009 MathSciNetCrossRefMATH

92.

Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 65–81. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_6 CrossRef

93.

Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. (TSE) 28(2), 183–200 (2002)CrossRef

94.

Zhang, X., Leucker, M., Dong, W.: Runtime verification with predictive semantics. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 418–432. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_37 CrossRef

Titel: Runtime Failure Prevention and Reaction
verfasst von: Yliès Falcone
Leonardo Mariani
Antoine Rollet
Saikat Saha
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_4

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