Proposal of an Algorithm to Generate VDM++ Specification Based on its Grammar by Using Word Lists Extracted from the Natural Language Specification

Authors
Tetsuro Katayama1, *, Yasuhiro Shigyo1, Yoshihiro Kita2, Hisaaki Yamaba1, Kentaro Aburada1, Naonobu Okazaki1
1Department of Computer Science and Systems Engineering, Faculty of Engineering, University of Miyazaki, 1-1 Gakuen-kibanadai nishi, Miyazaki, 889-2192 Japan
2Department of Information Security, Faculty of Information Systems, Siebold Campus, University of Nagasaki, 1-1-1 Manabino, Nagayo-cho, Nishi-Sonogi-gun, Nagasaki, 851-2195 Japan
*Corresponding author. Email: [email protected]
Corresponding Author
Tetsuro Katayama
Received 10 November 2019, Accepted 21 May 2020, Available Online 11 September 2020.
DOI
https://doi.org/10.2991/jrnal.k.200909.005
Keywords
Natural language specification; VDM++; automatic generation; formal method; formal specification
Abstract
The natural language includes ambiguous expressions. Vienna Development Method (VDM) is one of methodology on the formal methods to write the specification without ambiguity. Because VDM++ is written by strict grammar, it is difficult to write a VDM++ specification. This research attempts to generate a VDM++ specification automatically from a natural language specification by machine learning. To generate a VDM++ specification, it is necessary to extract words that consist of predicate corresponding to the function and nouns corresponding to variable from the natural language specification. This paper proposes an approach to generate a VDM++ specification based on its grammar from the classified word list. Identifiers are generated from the classified word list, and then the VDM++ specification can be generated by converting them into VDM++ grammar.
Copyright
© 2020 The Authors. Published by ALife Robotics Corp. Ltd..
Open Access
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)