A Transformation of Controlled Natural Language Behavioural Requirements into Modal Sequence Diagram Simulation Models for Requirement Conflict Detection

Abstract: PURPOSE: Specifying requirements in a semi-formal notation, such as a controlled natural language (CNL), allows reduction of ambiguity and underspecification in requirement specifications, as the notation uses well defined semantics and enforces consistency and conformance to syntactical rules. Contradicting requirements can be problematic to detect in practice depending on the size and complexity of the requirement specification. Requirement simulation is an opportunity to ameliorate the process of detecting inconsistency in requirement specifications. A formal requirement notation, unlike a semi-formal one, comes with the ability to perform requirement simulation. A formal notation, however, requires training and familiarity with formal methods in order to be understood, and this is not something that is suitable for every organisation. Yet, identifying and resolving conflicts between requirements early will help organisations reduce rework, i.e. nonessential efforts. If we can translate a set of requirements in a semi-formal notation into a formal notation, we facilitate the adoption of a useful practice in organisations that would not otherwise like to, or be able to, adopt formal methods. METHOD: The study adopts the methodology of design science research. Design science research addresses a specific problem that exists in at least one setting and proposes a product such as a model, a principle, a tool or a technique to solve this problem. In our case, the problem can be stated as translating semi-formal requirements into a formal notation for strengthening the scope of validation to include the detection of contradicting requirements in specifications. We use freely and publicly available requirements from the Economic Council of Europe and Daimler-Chrysler to show the application of our translation. These requirements come from a safety-critical requirements domain (the automotive industry) and describe behaviour of vehicular systems. As safety-critical systems have high safety requirements, we propose a consistent translation into simulation models, i.e. a mapping between one source model element into a target model element in a consistent way. We analyse the simulation models created by our transformation and discuss the feasibility of our approach. RESULTS: The results show that it is problematic to perform an accurate translation of semi-formal behavioural requirements specified on a higher level of abstraction with lower attention to specificity and detail comparatively into a formal notation describing precise details on a more concrete level for the purposes of simulation. Consequentially, a CNL describing behaviour with one specification approach can not fully capture all the information that is required by a fully automatic translation into a formal notation with a different specification approach, without first making essential improvements and necessary adjustments to account for the differences between the two specification approaches and to mimic numerous semantic elements from the formal notation onto the semi-formal notation. CONCLUSION: We propose that specifying requirements in a semi-formal notation to reduce ambiguity and underspecification in specifications, and then translating the requirements into a formal notation for inconsistency detection, is feasible. This can be applied in the automotive industry and elsewhere where it is considered useful to improve the ability of testing procedures to detect inconsistency in requirement specifications for the purpose of streamlining efforts. It is particularly important for safety-critical systems, where there could be serious consequences of an anomalous specification. Furthermore, we propose features of a semi-formal notation that is susceptible to translation into a formal notation for simulation purposes, which could be used as a starting point for adopting the tool suite that we introduce in this study.