Automated conversion from a requirements document to an executable formal specification

Many formal specification languages have been developed to engineer complex systems. However natural language (NL) has remained the choice of domain experts to specify the system because formal specification languages are not easy to master. Therefore NL requirements documentation must be reinterpreted by software engineers into a formal specification language. When the system is very complicated, which is mostly the case when one chooses to use formal specification, this conversion is both non-trivial and error-prone, if not implausible. This challenge comes from many factors such as miscommunication between domain experts and engineers. However the major bottleneck of this conversion is from the inborn characteristic of ambiguity of NL and the different level of the formalism between the two domains of NL and the formal specification. This is why there have been very few attempts to automate the conversion from requirements documentation to a formal specification language. This research project is developed as an application of formal specification and linguistic techniques to automate the conversion from a requirements document written in NL to a formal specification language. Contextual Natural Language Processing (CNLP) is used to handle the ambiguity problem in NL and Two Level Grammar (TLG) is used to deal with the different formalism level between NL and formal specification languages to achieve automated conversion from NL requirements documentation into a formal specification (in our case the Vienna Development Method - VDM++). A knowledge base is built from the NL requirements documentation using CNLP by parsing the documentation and storing the syntactic, semantic, and contextual information.