Thumbnail Image

Using behavioural specifications to support model-checking

Safety-critical interactive systems provide many benefits for human daily life, but erroneous safety-critical interactive systems can lead to serious consequences to the users. Thus building these systems requires that we ensure a high level of correctness. Formal models can be used to ensure that safetycritical systems are developed correctly. However, when models of the systems are being built, there is no guarantee that the modelled system fully satisfies the user requirements. If the systems are not what business stakeholders truly desire, new errors can be made. Behaviour-Driven-Development is often applied to ensure the requirements of thesystemareproperlyunderstoodandmaintainedbyusingBehaviouralSpecifications. These specifications use natural language, and so, are well suited for expressing user requirements. They can be used as the basis for test generation but do not provide the guarantees of correctness that formal methods can provide. In this work, we develop an approach that takes advantage of the expressivity of behaviour specifications and combines it with the use of formal methods. We use Behavioural Specifications to create First-Order-Logic predicates of the requirements. These predicates can be used with formal methods, either to support the creation of the formal models or to ensure the user requirements and specifications are consistent.
Type of thesis
Liu, B. (2019). Using behavioural specifications to support model-checking (Thesis, Master of Science (Research) (MSc(Research))). The University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/13028
The University of Waikato
All items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.