Show simple item record  

dc.contributor.advisorReeves, Steve
dc.contributor.advisorBowen, Judy
dc.contributor.authorJaidka, Sapna
dc.date.accessioned2020-08-31T04:10:55Z
dc.date.available2020-08-31T04:10:55Z
dc.date.issued2020
dc.identifier.citationJaidka, S. (2020). Formal modelling and analysis of safety-critical Interactive systems using Coloured Petri Nets (Thesis, Doctor of Philosophy (PhD)). The University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/13778en
dc.identifier.urihttps://hdl.handle.net/10289/13778
dc.description.abstractTo gain confidence in safety-critical interactive systems, formal modelling and analysis plays a vital role. Generally, existing techniques focus either on modelling the user interface or on modelling the functionality of a system. Although there are many benefits to using the individual models for different purposes, it requires a lot of work to do the coupling of functional behaviour with interactive elements for analysis. Therefore, further investigation into the modelling and analysis techniques was required that models all the parts (user interface, interaction and functional) into a single model. This research aims to apply formal methods for modelling and specifying the user interface, interaction and functional aspects of a safety-critical system in a single model using Coloured Petri Nets (CPN), then investigating the model to ensure that the system behaves as expected. The approach developed in this thesis has its starting point in several existing, accepted formal specification techniques. From this existing basis, we create a Coloured Petri Net model of a system which has the required features of existing formalisms, taking into account all three aspects (user interface, interaction and functional), hence our investigation of the combination of formalisms to achieve their combined strength. There are several reasons for using Coloured Petri Nets. Coloured Petri Nets provide a graphical representation and hierarchical structuring mechanism, and a state space verification technique, which allows querying the state space to investigate behaviours of a system. There are several tools that support Coloured Petri Nets including the CPN Tool which helps in building CPN models and allows simulation and analysis using state spaces. In this thesis, the findings of our investigation into modelling and analysis of safety-critical interactive systems are presented. We describe the technique developed to model and analyze an interactive system using Coloured Petri Nets. The technique is illustrated using a simplified infusion pump example. Then we present a case study of the Niki T34 Infusion Pump to show that we have retained all the expressiveness that we need of existing formalisms. Lastly, we present a small example of a nuclear reactor control system to show that now we can use the Coloured Petri Nets alone to model and analyze the user interface, interaction and functionality of safety-critical interactive systems and also to show that the scope of this technique is not limited to just the medical domain.
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
dc.subjectHuman Computer Interaction
dc.subjectColoured Petri Nets
dc.titleFormal modelling and analysis of safety-critical Interactive systems using Coloured Petri Nets
dc.typeThesis
thesis.degree.grantorThe University of Waikato
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy (PhD)
dc.date.updated2020-08-26T23:50:37Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record