Show simple item record  

dc.contributor.advisorBowen, Judy
dc.contributor.authorLiu, Bowen
dc.date.accessioned2019-10-24T02:06:56Z
dc.date.available2019-10-24T02:06:56Z
dc.date.issued2019
dc.identifier.citationLiu, 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/13028en
dc.identifier.urihttps://hdl.handle.net/10289/13028
dc.description.abstractSafety-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.
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherThe University of Waikato
dc.rightsAll items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
dc.subjectFormal methods,Cucumber,Behavioural Speficication
dc.titleUsing behavioural specifications to support model-checking
dc.typeThesis
thesis.degree.grantorThe University of Waikato
thesis.degree.levelMasters
thesis.degree.nameMaster of Science (Research) (MSc(Research))
dc.date.updated2019-10-24T02:05:35Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

This item appears in the following Collection(s)

Show simple item record