Abstract
Electronic inter-organizational relationships are governed by contracts regulating their interaction, therefore it is necessary to run-time monitor the contracts, as to guarantee their fulfillment. The present work shows how to obtain a run-time monitor for contracts written in \(\mathcal {CL}\), a formal specification language which allows to write conditional obligations, permissions, and prohibitions over actions. The trace semantics of \(\mathcal {CL}\) formalizes the notion of a trace fulfills a contract. We show how to obtain, for a given contract, an alternating Büchi automaton which accepts exactly the traces that fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for \(\mathcal {CL}\) contracts.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)
Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)
Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods in System Design 24(2), 101–127 (2004)
Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: STOC 1977, pp. 286–294. ACM, New York (1977)
Göller, S., Lohrey, M., Lutz, C.: PDL with Intersection and Converse Is 2 EXP-Complete. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 198–212. Springer, Heidelberg (2007)
Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)
Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)
Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by ∀-automata. In: POPL 1987, pp. 1–12 (1987)
Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: LICS 1988, pp. 422–427 (1988)
Pratt, V.R.: Process logic. In: POPL 1979, pp. 93–100. ACM Press, New York (1979)
Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 174–189. Springer, Heidelberg (2007)
Prisacariu, C., Schneider, G.: CL: A Logic for Reasoning about Legal Contracts – Semantics. Technical Report 371, Univ. Oslo (2008)
Prisacariu, C., Schneider, G.: Run-time Monitoring of Electronic Contracts – theoretical results. Technical report, Univ. Oslo (2008)
Stolz, V., Bodden, E.: Temporal Assertions Using AspectJ. In: RV 2005. ENTCS, vol. 144, pp. 109–124. Elsevier, Amsterdam (2006)
Vardi, M.Y.: Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191–206. Springer, Heidelberg (1997)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332–344 (1986)
von Wright, G.H.: Deontic logic. Mind 60, 1–15 (1951)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kyas, M., Prisacariu, C., Schneider, G. (2008). Run-Time Monitoring of Electronic Contracts. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)