scholarly journals FORMAL MODELING AND ANALYSIS OF ENTITY FRAMEWORK USING ALLOY

2021 ◽  
Vol 7 (2) ◽  
pp. 9-18
Author(s):  
Maria Belen Bonino ◽  
Ana Garis ◽  
Daniel Riesco
Keyword(s):  
Software Development ◽  
Automatic Generation ◽  
Formal Modeling ◽  
Validation And Verification ◽  
Modeling And Analysis ◽  
C Language ◽  
Design Defects ◽  
Industrial Adoption ◽  
Agile Software

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.

scholarly journals Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL

1997 ◽  
Vol 4 (31) ◽  
Author(s):  
Klaus Havelund ◽  
Arne Skou ◽  
Kim G. Larsen ◽  
Kristian Lund
Keyword(s):  
Software Development ◽  
Real Time ◽  
Real Life ◽  
Automatic Verification ◽  
Formal Modeling ◽  
Industrial Case Study ◽  
Modeling And Analysis ◽  
Audio Video ◽  
Assembler Code

A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose<br />is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on<br />real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However, using the real-time verification<br />tool UPPAAL, an error trace was automatically generated, which caused the detection of “the error” in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, it’s also an excellent example of the reverse impact.

Agile Software Development

2012 ◽  
pp. 1-15
Author(s):  
Torstein Nicolaysen ◽  
Richard Sassoon ◽  
Maria B. Line ◽  
Martin Gilje Jaatun
Keyword(s):  
Software Development ◽  
Agile Software Development ◽  
Agile Development ◽  
Implementation Team ◽  
Agile Methodologies ◽  
Development Organizations ◽  
Development Lifecycle ◽  
Software Development Lifecycle ◽  
Agile Software

In this article, the authors contrast the results of a series of interviews with agile software development organizations with a case study of a distributed agile development effort, focusing on how information security is taken care of in an agile context. The interviews indicate that small and medium-sized agile software development organizations do not use any particular methodology to achieve security goals, even when their software is web-facing and potential targets of attack. This case study confirms that even in cases where security is an articulated requirement, and where security design is fed as input to the implementation team, there is no guarantee that the end result meets the security objectives. The authors contend that security must be built as an intrinsic software property and emphasize the need for security awareness throughout the whole software development lifecycle. This paper suggests two extensions to agile methodologies that may contribute to ensuring focus on security during the complete lifecycle.

Fixed Priced Projects in Agile

2016 ◽  
pp. 222-236
Author(s):  
Anuradha Chaminda Gajanayaka
Keyword(s):  
Software Development ◽  
Agile Software Development ◽  
Development Model ◽  
Software Development Model ◽  
Responding To Change ◽  
The One ◽  
Agile Software ◽  
Development Methods ◽  
Software Development Methods

Agile software development has established as a reliable alternative to waterfall software development model. Unfortunately the use of agile software development has been limited to time based contracts and not for time limited contracts. The main reason for this limitation is the “Agile manifesto” itself. The forth value of the manifesto states that agile believers find more value in “Responding to change over following a plan”. This is the one of the main reasons why agile software development methods are not preferred for a fixed priced contract or time limited contract. The following case study provides an example on how the agile software development can be used for fixed priced software development contracts even when operating in offshore context. The agile software development concepts were used throughout to plan, execute, monitor, report, etc. for the project documented in this case study.

scholarly journals Formal Modeling and Analysis of Fairness Characterization of E-Commerce Protocols

2014 ◽  
Vol 2014 ◽  
pp. 1-10
Author(s):  
Chengwei Zhang ◽  
Xiaohong Li ◽  
Jing Hu ◽  
Zhiyong Feng ◽  
Jiaojiao Song
Keyword(s):  
Formal Modeling ◽  
Sufficient Condition ◽  
Formal Approach ◽  
Common Assumption ◽  
Modeling And Analysis ◽  
Verification Method ◽  
Space Model ◽  
The Past

In the past, fairness verification of exchanges between the traders in E-commerce was based on a common assumption, so-called nonrepudiation property, which says that if the parties involved can deny that they have received or sent some information, then the exchanging protocol is unfair. So, the nonrepudiation property is not a sufficient condition. In this paper, we formulate a new notion of fairness verification based on the strand space model and propose a method for fairness verification, which can potentially determine whether evidences have been forged in transactions. We first present an innovative formal approach not to depend on nonrepudiation, and then establish a relative trader model and extend the strand space model in accordance with traders’ behaviors of E-commerce. We present a case study to demonstrate the effectiveness of our verification method.

Teaching Agile Software Development: A Case Study

2011 ◽  
Vol 54 (2) ◽  
pp. 273-278 ◽  
Author(s):  
Vladan Devedžić ◽  
Saša R Milenković
Keyword(s):  
Software Development ◽  
Agile Software Development ◽  
Agile Software
Sign in / Sign up

Export Citation Format

Share Document