Panagiotis Katsaros, University of Thessaloniki, Greece
Formalisation and analysis of natural language system requirements
Abstract:
System requirements constitute a partial specification of a system under design. Starting with such a specification in natural language, which is usually restricted in syntax terms, we are interested to provide early evidence that costly cycles of corrections (in design, implementation and verification/validation), due to inadequate system specification, will be avoided. Requirements formalisation is a necessary step in this: the requirements are transformed into a specification with unique interpretation, through resolving ambiguities and underspecified references, as well as assessing whether they are consistent, correct (i.e. valid for an acceptable solution) and attainable. Finally, the requirements should be possible to be formally verified.
According to our view, formalisation is a two-stage model-driven process that involves using requirement boilerplates for specifying requirements, i.e. textual templates to be filled with ontology concepts for expressing them (i) based on a semantic model of the system domain, and (ii) with respect to a formal model of the system’s design (derivation of formal properties), i.e. an abstracted representation in a specification language with formal semantics. During the stage (i), a series of semantic analyses is enabled (detect inconsistencies, ambiguity, redundancy, noise and incompleteness), which guide the engineer for improving the requirement specification, as well as for eliciting tacit knowledge. The problems addressed in this stage are a prerequisite to enable the derivation of formal specifications in a logic language. Properties derivation (stage ii) is semi-automated, through having associated requirement boilerplates with property patterns in restricted natural language. Each pattern has been defined semantics in a logic language and the requirement terms/concepts have to be mapped to states and events of the system’s formal model. This ensures that requirements have a consistent interpretation with respect to the system’s model and eventually enables a series of additional analyses to detect sets of properties (and associated requirements) that may be unsatisfiable or not realisable. If some properties are not satisfied by the model, then a modified design (and model) has to be pursued or the requirements that are not satisfied have to be refined.
Our approach is tool-supported and it has been applied to the formalisation of industrial requirements for space systems. Very recently, it has been extended towards formalising requirements for failures, detection, isolation and recovery (FDIR), as well as requirements for autonomous systems with learning-enabled components, which usually generate monitorable/enforceable properties at runtime.
Slides :
Available here