nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Runtime Verification of Contracts with Themulus

verfasst von : Alberto Aranda García, María-Emilia Cambronero, Christian Colombo, Luis Llana, Gordon J. Pace

Erschienen in: Software Engineering and Formal Methods

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

Contracts regulating the behaviour of multiple interacting parties go beyond the notion of pure properties, but allow one to document and analyse the ideal behaviour. In this paper we build upon a real-time deontic logic allowing the description of such contracts and present a runtime verification tool for monitoring of such contracts. We present a verification algorithm used to monitor contracts written in this logic and an airport agreement is used as a case study to illustrate how such agreements and contracts can be monitored using our tool with reasonable processing costs.

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 Synthesis of P-Stable Abstractions

Nächstes Kapitel Sound C Code Decompilation for a Subset of x86-64 Binaries

It is worth noting that the logic we present works equally well if the natural numbers are used for a discrete time domain. However, we allow for real time values to cater for any temporal constraints.

We write r; s to indicate the forward composition of the two relations r and s, and use \(\longmapsto \) to denote the reflexive transitive closure of the timed labelled transition systems.

By Zeno-like behaviour, we mean an infinite number of arbitrarily smaller time steps whose sum converges, thus blocking time from progressing.

Code is available at: https://github.com/aarandag/larva-timedcontracts.

Madrid-Barajas Airport. Airport Regulations (2020). https://www.aeropuertomadrid-barajas.com/eng/air-passenger-rights.htm. https://www.aeropuertomadrid-barajas.com/eng/regulations-hand-luggage.htm. https://www.aeropuertomadrid-barajas.com/eng/checkin-madrid-airport.htm. Accessed 25 May 2020

García, A.A., Cambronero, M.E., Colombo, C., Llana, L., Pace, G.J.: Themulus: a timed contract-calculus. In: Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, pp. 193–204 (2020)

García, A.A., Cambronero, M.E., Colombo, C., Llana, L., Pace, G.J.: Themulus: a timed contract-calculus. Technical Report TR-01-20, Universidad Complutense de Madrid (2020)

Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)MathSciNetCrossRef

Chen, F., Rosu, G.: MOP: an efficient and generic runtime verification framework. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, Montreal, Quebec, Canada, 21–25 October 2007, pp. 569–588 (2007)

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_13CrossRef

Cranefield, S.: A rule language for modelling and monitoring social expectations in multi-agent systems. In: Boissier, O., et al. (eds.) AAMAS 2005. LNCS (LNAI), vol. 3913, pp. 246–258. Springer, Heidelberg (2006). https://doi.org/10.1007/11775331_17CrossRef

Dastani, M., Torroni, P., Yorke-Smith, N.: Monitoring norms: a multi-disciplinary perspective. Knowl. Eng. Rev. 33, e25 (2018)CrossRef

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

10.

Wright, G.H.V.: Deontic logic. Mind 60(237), 1–15 (1951)CrossRef

11.

Governatori, G., Rotolo, A., Sartor, G.: Temporalised normative positions in defeasible logic. In: The Tenth International Conference on Artificial Intelligence and Law, Proceedings of the Conference, Bologna, Italy, 6–11 June 2005, pp. 25–34 (2005)

12.

Hashmi, M., Governatori, G., Wynn, M.T.: Modeling obligations with event-calculus. In: Bikakis, A., Fodor, P., Roman, D. (eds.) RuleML 2014. LNCS, vol. 8620, pp. 296–310. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09870-8_22CrossRef

13.

Pace, G.J., Schapachnik, F.: Contracts for interacting two-party systems. In: FLACOS 2012. ENTCS, vol. 94, pp. 21–30 (2012)

14.

Pace, G.J., Schneider, G.: Challenges in the specification of full contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 292–306. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00255-7_20CrossRef

15.

Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Logic Algebraic Program. 81(4), 458–490 (2012). Special Issue: NWPT 2009

16.

Testerink, B., Dastani, M., Meyer, J.-J.Ch.: Norm monitoring through observation sharing. In: Proceedings of the European Conference on Social Intelligence, ECSI-2014, Barcelona, Spain, 3–5 November 2014, pp. 291–304 (2014)

17.

Yi, W.: CCS + time = an interleaving model for real time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54233-7_136CrossRef

Titel: Runtime Verification of Contracts with Themulus
verfasst von: Alberto Aranda García
María-Emilia Cambronero
Christian Colombo
Luis Llana
Gordon J. Pace
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-58767-3

Electronic ISBN: 978-3-030-58768-0

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-58768-0_13

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"