Top

Published in:

2014 | OriginalPaper | Chapter

Symbolic Termination and Confluence Checking for ECA Rules

Authors : Xiaoqing Jin, Yousra Lembachar, Gianfranco Ciardo

Published in: Transactions on Petri Nets and Other Models of Concurrency IX

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Event-condition-action (ECA) rules can specify decision processes and are widely used in reactive systems and active database systems. Applying formal verification techniques to guarantee properties of the designed ECA rules is essential to help the error-prone procedure of collecting and translating expert knowledge. However, while the nondeterministic and concurrent semantics of ECA rule execution enhances expressiveness, it also makes analysis and verification more difficult. We propose an approach to analyze the dynamic behavior of a set of ECA rules, by first translating them into an extended Petri net, then studying two fundamental correctness properties: termination and confluence. Our experimental results show that the symbolic algorithms we present greatly improve scalability.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter A Canonical Contraction for Safe Petri Nets

next chapter Tissue Systems and Petri Net Synthesis

Abadi, D.J., Carney, D., Çetintemel, U., Cherniack, M., Convey, C., Lee, S., Stonebraker, M., Tatbul, N., Zdonik, S.: Aurora: a new model and architecture for data stream management. VLDB J. 12(2), 120–139 (2003)CrossRef

Aiken, A., Widom, J., Hellerstein, J.M.: Behavior of database production rules: termination, confluence, and observable determinism. In: Proceedings of the ACM SIGMOD International Conference on Management of Data, pp. 59–68. ACM Press (1992)

Augusto, J.C., Nugent, C.D.: A new architecture for smart homes based on ADB and temporal reasoning. In: Toward a Human-Friendly Assistive Environment, vol. 14, pp. 106–113 (2004)

Baralis, E., Ceri, S., Paraboschi, S.: Improved rule analysis by means of triggering and activation graphs. In: Sellis, T.K. (ed.) RIDS 1995. LNCS, vol. 985, pp. 163–181. Springer, Heidelberg (1995)CrossRef

Baralis, E., Widom, J.: An algebraic approach to static analysis of active database rules. ACM Trans. Database Syst. 25(3), 269–332 (2000)CrossRef

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATH

Choi, E.-H., Tsuchiya, T., Kikuno, T.: Model checking active database rules under various rule processing strategies. IPSJ Digit. Cour. 2, 826–839 (2006)CrossRef

Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.I.: Logical and stochastic modeling with Smart. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78–97. Springer, Heidelberg (2003)CrossRef

Ciardo, G., Lüttgen, G., Siminiceanu, R.I.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)CrossRef

10.

Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 51–95. Springer, Heidelberg (2012)CrossRef

11.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

12.

Comai, S., Tanca, L.: Termination and confluence by rule prioritization. IEEE Trans. Knowl. Data Eng. 15, 257–270 (2003)CrossRef

13.

French, T.: Decidability of propositionally quantified logics of knowledge. In: Gedeon, T.T.D., Fung, L.C.C. (eds.) AI 2003. LNCS (LNAI), vol. 2903, pp. 352–363. Springer, Heidelberg (2003)

14.

Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1–2), 9–62 (1998)MATHMathSciNet

15.

Kulkarni, K.G., Mattos, N.M., Cochrane, R.: Active database features in SQL3. In: Paton, N.W. (ed.) Active Rules in Database Systems, pp. 197–219. Springer, New York (1999)CrossRef

16.

Lee, E.A.: Computing foundations and practice for cyber-physical systems: a preliminary report. Technical report UCB/EECS-2007-72, University of California, Berkeley, May 2007

17.

Li, X., Medina Marín, J., Chapa, S.V.: A structural model of ECA rules in active database. In: Coello Coello, C.A., de Albornoz, Á., Sucar, L.E., Battistutti, O.C. (eds.) MICAI 2002. LNCS (LNAI), vol. 2313, pp. 486–493. Springer, Heidelberg (2002)

18.

McCarthy, D., Dayal, U.: The architecture of an active database management system. ACM Sigmod Rec. 18(2), 215–224 (1989)CrossRef

19.

Murata, T.: Petri nets: properties, analysis and applications. Proc. of the IEEE 77(4), 541–579 (1989)CrossRef

20.

Nazareth, D.: Investigating the applicability of petri nets for rule-based system verification. IEEE Trans. Knowl. Data Eng. 5(3), 402–415 (1993)CrossRef

21.

Ray, I., Ray, I.: Detecting termination of active database rules using symbolic model checking. In: Caplinskas, A., Eder, J. (eds.) ADBIS 2001. LNCS, vol. 2151, pp. 266–279. Springer, Heidelberg (2001)CrossRef

22.

Valk, R.: Generalizations of petri nets. In: Gruska, J., Chytil, M.P. (eds.) MFCS 1981. LNCS, vol. 118, pp. 140–155. Springer, Heidelberg (1981)CrossRef

23.

Varró, D.: A formal semantics of uml statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 378–392. Springer, Heidelberg (2002)CrossRef

24.

Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368–381. Springer, Heidelberg (2009)CrossRef

25.

Zhao, Y., Ciardo, G.: Symbolic computation of strongly connected components and fair cycles using saturation. Innov. Syst. Softw. Eng. 7(2), 141–150 (2011)CrossRef

26.

Zhao, Y., Xiaoqing, J., Ciardo, G.: A symbolic algorithm for shortest EG witness generation. In: Proceedings of TASE, pp. 68–75. IEEE Computer Society Press (2011)

Title: Symbolic Termination and Confluence Checking for ECA Rules
Authors: Xiaoqing Jin
Yousra Lembachar
Gianfranco Ciardo
Publisher: Springer Berlin Heidelberg
Book: Transactions on Petri Nets and Other Models of Concurrency IX
Print ISBN: 978-3-662-45729-0

Electronic ISBN: 978-3-662-45730-6

Copyright Year: 2014
DOI: https://doi.org/10.1007/978-3-662-45730-6_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner