Using behavioural specifications to support model-checking
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
Permanent Research Commons link: https://hdl.handle.net/10289/13028
Safety-critical interactive systems provide many beneﬁts 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 satisﬁes 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 thesystemareproperlyunderstoodandmaintainedbyusingBehaviouralSpeciﬁcations. These speciﬁcations 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 speciﬁcations and combines it with the use of formal methods. We use Behavioural Speciﬁcations 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 speciﬁcations are consistent.
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.
- Masters Degree Theses