Abstract
Model checking, as one area of formal verification, is recently subject of an intensive research. Many verification tools intended to check properties of models of systems were developed, mainly at universities. Many researches are also interested in real-time database management systems (RTDBMS). In this paper we show some possibilities of using a verification tool Uppaal on some variants of priority assignment algorithms used in RTDBMS. We present some possible models of such algorithms expressed as nets of timed automata, which are a modeling language of Uppaal and then some simulation and verification possibilities of Uppaal on those models.
This is a preview of subscription content, log in via an institution to check access.
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
Abbott, R.K., Garcia-Molina, H.: Scheduling real-time transactions: a performance evaluation. ACM Transactions on Database Systems (TODS) 17(3), 513–560 (1992)
Alur, R., Dill, D.L.: Automata for modeling real-time systems. Proc. of Int. Colloquium on Algorithms, Languages, and Programming. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Behrmann, G., David, A., Larsen, K. G.: A Tutorial on Uppaal (December 15, 2008), http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf
Berard, B., Bidoit, M., Petit, A., Laroussinie, F., Petrucci, L., Schnoebelen, P.: Systems and Software Verification, Model-Checking Techniques and Tools. Springer, Heidelberg (2001); ISBN: 978-3540415237
David, A., Amnell, T.: Uppaal2k: Small Tutorial (December 15, 2008), http://www.it.uu.se/research/group/darts/uppaal/tutorial.ps
Haritsa, J.R., Livny, M., Carey, M.J.: Earliest Deadline Scheduling for Real-Time Database Systems. In: Proceedings of Real-Time Systems Symposium 1991, pp. 232–242 (1991); ISBN: 0-8186-2450-7
Henzinger, T.A.: Symbolic model checking for real-time systems. Information and computation 111, 193–244 (1994)
Kao, B., Garcia-Molina, H.: An Overview of Real-Time Database Systems. In: Advances in Real-Time Systems, pp. 463–486. Prentice-Hall, Inc., Englewood Cliffs (1995)
Kot, M.: Modeling selected real-time database concurrency control protocols in Uppaal. Innovations in Systems and Software Engineering 5(2), 129–138 (2009); ISSN: 1614-5046
Kot, M.: Modeling Real-Time Database Concurrency Control Protocol Two-Phase-Locking in Uppaal. In: Proceedings of the International Multiconference on Computer Science and Information Technology, vol. 3, pp. 673–678. IEEE Computer Society Press, Los Alamitos (2008); ISBN: 978-83-60810-14-9, ISSN: 1896-7094
Kot, M.: Modeling and Verification of Priority Assignment in Real-Time Databases Using Uppaal. In: Proceedings of the Dateso 2010 Annual International Workshop on DAtabases, TExts, Specifications and Objects, CEUR Workshops Proceedings, Sun SITE Central Europe, vol. 567, pp. 147–154 (2010); ISSN: 1613-0073
Król, V., Pokorný, J., Černohorský, J.: The V4DB project - support platform for testing the algorithms used in real-time databases. WSEAS Transactions on Information Science & Applications 10(3) (October 2006)
McMillan, K.L.: Symbolic Model Checking. Springer, Heidelberg (1993); ISBN: 978-0792393801
Neto, P.F.R., Perkusich, M.L.B., De Almeida, H.O., Perkusich, A.: A Formal Verification and Approach for Real-Time Databases. Selected Readings on Database Technologies and Applications, Information Science Reference, 268–295 (2009); ISBN: 978-1-60566-098-1
Nyström, D., Nolin, M., Tesanovic, A., Norström, C., Hansson, J.: Pessimistic Concurrency-Control and Versioning to Support Database Pointers in Real-Time Databases. In: Proc. of the 16th Euromicro Conference on Real-Time Systems, pp. 261–270. IEEE Computer Society, Los Alamitos (2004)
Ulusoy, Ö., Belford, G.G.: A Simulation Model for Distributed Real-Time Database Systems. In: Proceedings of the 25th Annual Simulation Symposium, pp. 232–240 (1992); ISBN: 0-8186-2765-4
ParaDiSe (Parallel & Distributed Systems Laboratory): Yahoda verification tools database (April 15, 2011), http://anna.fi.muni.cz/yahoda/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kot, M. (2011). Using Uppaal for Verification of Priority Assignment in Real-Time Databases. In: Snasel, V., Platos, J., El-Qawasmeh, E. (eds) Digital Information Processing and Communications. ICDIPC 2011. Communications in Computer and Information Science, vol 189. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22410-2_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-22410-2_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22409-6
Online ISBN: 978-3-642-22410-2
eBook Packages: Computer ScienceComputer Science (R0)