Open AccessFormal Modeling and Analysis of Entity Framework Using Alloy
Author(s) -
Maria Belen Bonino,
Ana Gabriela Garis,
Daniel Eduardo Riesco
Publication year - 2021
Publication title -
international journal of software engineering and computer systems
Language(s) - English
Resource type - Journals
eISSN - 2289-8522
pISSN - 2180-0650
DOI - 10.15282/ijsecs.7.2.2021.2.0085
Subject(s) - computer science , agile software development , software engineering , modeling language , flexibility (engineering) , domain (mathematical analysis) , software development , systems engineering , software , software development process , programming language , engineering , mathematical analysis , statistics , mathematics
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.