tailieunhanh - Model checking early requirements specifications in alloy

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. | Journal of Science and Technology 54 (3A) (2016) 163-175 MODEL CHECKING EARLY REQUIREMENTS SPECIFICATIONS IN ALLOY Ton Long Phuoc*, Nguyen Minh Hai Department of Information and Technology, Industrial University of HCMC , 12 Nguyen Van Bao, Ward 4, Go Vap District, Ho Chi Minh City Email: tonlongphuoc@ Received: 15 June 2015; Accepted for publication: 28 July 2016 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. Keywords: MVC, DSL, alloy, code generation. 1. INTRODUCTION One of the main activities of any development process aimed at creating useful software is domain modeling. Domain is the business processes being automated or the real world problem being solved by a software program. Having a good understanding of a software domain is essential for the success of any software development project. Software domains, being part of the real world, are hard to be captured directly. They have to be modeled using appropriate abstractions. Because of the great amount of knowledge related to any subject area, a domain model has to be a selection of that knowledge and .