Temporal Controlled Natural Language for Formal Specification

Abstract

Formal specifications describe behaviours and properties of embedded systems within a wide range of settings, i.e. from portable mobile devices, such as smartphones and tablets, to large stationary installations such as MRI machines and automobiles. These formal specifications are statements expressed in a temporal logic. Moreover, the formal specifications help to detect problems in system requirements by verifying the correctness of systems with respect to their formal specifications through automated reasoning tools. With the growing complexity of embedded system designs, industries employ formal specifications to verify the implementation of systems to reduce space, power and costs. In recent years, controlled natural language, which is a subset of natural language with restricted syntax and semantics, is used to extract formal specifications from natural language specifications for embedded systems. Controlled natural language can reduce ambiguity and eliminate the complexity of natural language specifications. However, after the critical analysis of existing proposals in literature with regard to generating formal specifications from natural language specifications, we have observed that there is a lack of scalable tools for capturing temporal constructions in natural language specifications. This thesis presents a scalable controlled natural language for generating formal specifications from natural language specifications featuring temporal constructions. These constructions are one of the greatest challenges in this field, since there are many obstacles within the field of the temporal semantics of natural languages, such as tenses, aspects and temporal prepositions. We examine a variety of formal semantics of temporal constructions in literature. However, there are still many varieties of temporal expressions in English which these existing theories cannot account for. Therefore, we exploit and extend an interval temporal logic, called TPL, to capture formally a range of temporal constructions that are often featured in natural language specifications. The logic TPL has variables which range over time-intervals and predicates corresponding to event-types and temporal order-relations. We then construct a transformation method that maps TPL into our desired formal specifications. TPL makes the transformations from natural language descriptions to formal specification possible since TPL has enough expressive power to deal with most temporal constructions commonly encountered in natural language specifications. We are able to prove the translation from TPL to formal specification theoretically. We also demonstrate the efficiency of our method in practice, which shows enormous performance improvements in comparison to known tools.

Date of Award	1 Aug 2018
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Allan Ramsay (Supervisor) & Ian Pratt-Hartmann (Supervisor)