FORMAL MODELING AND ANALYSIS OF ENTITY FRAMEWORK USING ALLOY
DOI:
https://doi.org/10.15282/ijsecs.7.2.2021.2.0085Keywords:
Alloy, Entity Framework, Formal Methods, Agile Methods, C#Abstract
Formal methods provide multiple benefits when applied in the software development process. For instance, they enable engineers to verify and validate models before working on their implementation, leading to earlier detection of design defects. However, most of them lack flexibility to be applied in agile software development projects. Alloy is a lightweight formal modeling language with a friendly tool that facilitates the agile approaches application. Unfortunately, its industrial adoption is hampered by the lack of methods and tools for current software development frameworks, such as Entity Framework. This platform is usually chosen by agile projects following the code-first approach that allows automatic generation of a database from domain classes coded in the C# language. We present a new method and tool for the formal specification and analysis of Entity Framework projects with Alloy. The proposal allows engineers to start the software development using Alloy for modeling, validation and verification, automatically translate Alloy specifications to C# domain classes and then generate the corresponding database with Entity Framework. We validate our approach with a real case study: an application required by a gas supplier company.
References
Entity Framework Tutorial. (n.d.). Entity Data Model. Retrieved from What is code-first?:
https://www.entityframeworktutorial.net/code-first/what-is-code-first.aspx
Black, S., Boca, P. P., Bowen, P. J., Gorman, J. & Hinchey, M. (2009). Formal Versus Agile: Survival of the Fittest?. IEEE
Computer, Vol. 42, No. 9, pp. 37-45.
Beedle, M., Beck, K., Bennekum, A. v., Cockburn, A., Cunningham, W., Fowler, M., Thomas, D. (2001). Manifesto for agile
software development. Retrieved from https://agilemanifesto.org/
Chul-Wuk, J., Il-Gon, K., & Choi, J.-Y. (2005). Automatic generation of the c# code for security protocols verified with
casper/fdr. In Proceedings of the 9th International Conference on Advanced Information Networking and Applications, Vol.
, pp. 507–510.
Cunha, A., Garis, A., & Riesco, D. (2015). Translating between Alloy specifications and UML class diagrams annotated with
OCL. Software & Systems Modeling, Springer. Vol. 14, pp. 1-21.
Cunha, A., & Pacheco, H. (2009). Mapping between Alloy specifications and database implementations. In Proceedings of
the 7th IEEE International Conference on Software Engineering and Formal Methods, pp. 285-294.
Cunha, A. (2016). Alloymda. Retrieved from https://sourceforge.net/projects/alloymda/
Entity Framework Tutorial (2019). Tutorial: Get Started with Entity Framework 6 Code First using MVC 5. Retrieved from
Entity Framework Tutorial. (2020). Retrieved from DbContext in Entity Framework 6:
https://www.entityframeworktutorial.net/entityframework6/dbcontext.aspx
Kant P., Hammond K., Coutts D., Chapman J., Clarke N., Corduan J. & Davies N. (2020). Flexible Formality Practical
Experience with Agile Formal Methods. In Proceedings of the 21st International Symposium of Trends in Functional
Programming. TFP 2020. Springer. Vol. 12222. pp. 94-120.
Krings, S., Schmidt, J., Brings, C., Frappier, M., & Leuschel, M. (2018). A Translation from Alloy to B. In Proceedings of
the 6th International Conference Abstract State Machines, Alloy, B, TLA, VDM, and Z. Springer. Vol. 10817, pp. 71-86.
Krishnamurthi, S., Fisler, K., Dougherty, D. J., & Yoo, D. (2008). Alchemy: Transmuting base Alloy specifications into
implementations. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software
engineering, pp. 158-169.
Khurshid, S., & Marinov, D. (2001). Testera: A novel framework for testing java programs. In Proceedings of the 16th Annual
International Conference on IEEE International Conference on Automated Software Engineering.
Garavel H., ter Beek M. & van de Pol J. (2020). The 2020 Expert Survey on FormalMethods. In Proceedings of the
International Conference on Formal Methods for Industrial Critical Systems FMICS 2020: Formal Methods for Industrial
Critical Systems. pp 3-69.
Huisman, M., Gurov, D., Malkis, A. (2020). Formal methods: from academia to industrial practice. A travel guide. CoRR.
Vol. abs/2002.07279. https://arxiv.org/abs/2002.07279
Indrakshi, R., Geri, G., Kyriakos, A., & Behzad, B. (2010). On Challenges of Model Transformation from UML to Alloy.
Software & Systems Modeling. Vol. 9, pp. 69-86.
Jackson, D. (2012). Software Abstractions: Logic, Language, and Analysis (Revised edition). MIT Press.
Laribee, D. (2009, 02). Microsoft Docs. Retrieved from Best Practice - An Introduction To Domain-Driven Design:
Microsoft. (2016) Microsoft Docs. Retrieved from Code First Migrations: https://docs.microsoft.com/enus/ef/ef6/modeling/code-first/migrations/?redirectedfrom=MSDN
Microsoft. (2020a). Entity Framework Core. Retrieved from https://docs.microsoft.com/en-us/ef/core/
Microsoft. (2020b). Introduction to projects and solutions. Retrieved from https://docs.microsoft.com/en-us/visualstudio/getstarted/tutorial-projects-solutions?view=vs-2019
Steffen, B. (2017). The physics of software tools: SWOT analysis and vision. Int. J. Softw. Tools Technol. Transfer. Vol. 19,
pp. 1–7.
Vaziri, M., & Jackson, D. (2003). Checking properties of heap-manipulating procedures with a constraint solver. In
Proceedings of 16th Annual International Conference on IEEE International Conference on Automated Software Engineering,
Vol. 2619, pp. 505-520.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2021 Maria Belen Bonino, Ana Garis, Daniel Riesco
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
