MODEL CHECKING EARLY REQUIREMENTS SPECIFICATIONS IN ALLOY

Authors

  • Ton Long Phuoc Department of Information and Technology, Industrial University of HCMC , 12 Nguyen Van Bao, Ward 4, Go Vap District, Ho Chi Minh City

DOI:

https://doi.org/10.15625/2525-2518/54/3A/11968

Keywords:

MVC, DSL, alloy, code generation.

Abstract

Automation generated source code and verifying are essential sector for software engineering. There are many ways to generate source code and verify from the specification languages. In this paper, we propose an approach that automatically generated code from a specification language Alloy. From this specification language, we will describe how to translate from one language to the Java source. An application in this paper is a gardening game program. Applied after the findings will be organized according to the MVC (Model-View-Controller) architectural pattern. Besides, we will also verify the identity of the structure of the application and the content of the Alloy specification. We built an tool as GmDSL, we have verified the aplication in GmDSL. The application was created from the tool also shows the correctness of the early constraints. Simultaneously, we also compares be verified through the GmDSL tool with NuSVM tool.

Downloads

Download data is not yet available.

Downloads

Published

2018-03-20

Issue

Section

Articles