To 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.