nach oben

vorheriges Kapitel A Canonical Contraction for Safe Petri Nets

nächstes Kapitel Tissue Systems and Petri Net Synthesis

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2014 | OriginalPaper | Buchkapitel

Symbolic Termination and Confluence Checking for ECA Rules

Erstes Kapitel lesen

Autoren: Xiaoqing Jin, Yousra Lembachar, Gianfranco Ciardo

Verlag: Springer Berlin Heidelberg

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

» Jetzt Zugang zum Volltext erhalten

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

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)

Titel

Symbolic Termination and Confluence Checking for ECA Rules

Buch

Transactions on Petri Nets and Other Models of Concurrency IX

Print ISBN: 978-3-662-45729-0

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

https://doi.org/10.1007/978-3-662-45730-6

DOI

https://doi.org/10.1007/978-3-662-45730-6_6

Autoren:

Xiaoqing Jin
Yousra Lembachar
Gianfranco Ciardo

Verlag

Springer Berlin Heidelberg

Sequenznummer

Premium Partner

Bildnachweise