MODEL CHECKING EARLY REQUIREMENTS SPECIFICATIONS IN ALLOY
Keywords:MVC, DSL, alloy, code generation.
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.
Authors who publish with Vietnam Journal of Science and Technology agree with the following terms:
- The manuscript is not under consideration for publication elsewhere. When a manuscript is accepted for publication, the author agrees to automatic transfer of the copyright to the editorial office.
- The manuscript should not be published elsewhere in any language without the consent of the copyright holders. Authors have the right to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal’s published version of their work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are encouraged to post their work online (e.g., in institutional repositories or on their websites) prior to or during the submission process, as it can lead to productive exchanges or/and greater number of citation to the to-be-published work (See The Effect of Open Access).