Abstract
Data-management applications are focused around so-called CRUD actions that create, read, update, and delete data from persistent storage. These operations are the building blocks for numerous applications, for example dynamic websites where users create accounts, store and update information, and receive customized views based on their stored data. Typically, the application’s data is required to satisfy some properties, which we may call the application’s data invariants. In this paper, we introduce a tool-supported, model-based methodology for proving that all the actions possibly triggered by a data-management application will indeed preserve the application’s data invariants. Moreover, we report on our experience applying this methodology on a non-trivial case study: namely, an application for managing medical records, for which over eighty data invariants need to be proved to be preserved.
This work is partially supported by the Spanish Ministry of Economy and Competitiveness Project “StrongSoft” (TIN2012-39391-C04-01 and TIN2012-39391-C04-04).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Basin, D., Doser, J., Lodderstedt, T.: Model driven security: From UML models to access control infrastructures. ACM Transactions on Software Engineering and Methodology 15(1), 39–91 (2006)
Basin, D.A., Clavel, M., Egea, M., García de Dios, M.A., Dania, C.: A model-driven methodology for developing secure data-management applications. IEEE Trans. Software Eng. 40(4), 324–337 (2014)
Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software 83(2), 283–302 (2010)
Clavel, M., Egea, M., García de Dios, M.A.: Checking unsatisfiability for OCL constraints. Electronic Communications of the EASST 24, 1–13 (2009)
Dania, C., Clavel, M.: OCL2FOL+: Coping with Undefinedness. In: Cabot, J., Gogolla, M., Ráth, I., Willink, E. (eds.) CEUR Workshop Proceedings OCL@MoDELS, vol. 1092, pp. 53–62. CEUR-WS.org (2013)
García de Dios, M.A., Dania, C., Basin, D., Clavel, M.: Model-driven development of a secure eHealth application. In: Heisel, M., Joosen, W., Lopez, J., Martinelli, F. (eds.) Engineering Secure Future Internet Services and Systems. LNCS, vol. 8431, pp. 97–118. Springer, Heidelberg (2014)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
D’Souza, D., Wills, A.: Catalysis. Practical Rigor and Refinement: Extending OMT, Fusion, and Objectory. Technical report (1995), http://catalysis.org
Gogolla, M., Hamann, L., Hilken, F., Kuhlmann, M., France, R.B.: From application models to filmstrip models: An approach to automatic validation of model dynamics. In: Fill, H., Karagiannis, D., Reimer, U. (eds.) Modellierung. LNI, vol. 225, pp. 273–288. GI (2014)
González, C.A., Cabot, J.: Formal verification of static software models in MDE: A systematic review. Information & Software Technology 56(8), 821–838 (2014)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)
Kanso, B., Taha, S.: Temporal constraint support for OCL. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol. 7745, pp. 83–103. Springer, Heidelberg (2013)
Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)
NESSoS. The European Network of Excellence on Engineering Secure Future internet Software Services and Systems (2010), http://www.nessos-project.eu
Object Management Group. Object constraint language specification version 2.4. Technical report, OMG (2014), http://www.omg.org/spec/OCL/2.4
Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: Finite reasoning on UML/OCL conceptual schemas. Data & Knowledge Engineering 73, 1–22 (2012)
Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using Boolean satisfiability. In: DATE, pp. 1341–1344. IEEE (2010)
WieringaA, R.: survey of structured and object-oriented software specification methods and techniques. ACM Comput. Surv. 30(4), 459–527 (1998)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dania, C., Clavel, M. (2015). Model-Based Formal Reasoning about Data-Management Applications. In: Egyed, A., Schaefer, I. (eds) Fundamental Approaches to Software Engineering. FASE 2015. Lecture Notes in Computer Science(), vol 9033. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46675-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-46675-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46674-2
Online ISBN: 978-3-662-46675-9
eBook Packages: Computer ScienceComputer Science (R0)