During the past years, software has become a large part of our personal and professional lives. We rely increasingly more on different kinds of applications to support our daily routines. Although failures in most of the applications we use do not have severe consequences, errors in some of the systems may cause damage to the environment, people, or economics and, in the worst case, human loss. For such safety-critical systems, it is crucial to ensure that they function correctly to reduce the risk of error occurrence. Various safety standards specify requirements for the software development process that should lead to more reliable software. However, meeting these requirements often increases the costs and development time. At the same time, many businesses require the software development and delivery process to be as fast and cheap as possible in order to survive in competitive environments.
This thesis addresses the trade-off between faster software development and the quality of the final product and discusses how modelling and verification can contribute to satisfying safety standard requirements. We use Tellu Diabetes App, a mobile application that forms a part of a safety-critical Internet of Things system, as a use case. The modelling and verification process is carried out with the help of DCR Graphs, a form of mathematical notation that has previously been used for modelling and reasoning about business processes. In the thesis, we construct and verify models of the process of making changes to the application code and the Tellu Diabetes App. For each of the models, we discuss which parts of the safety standard requirements it contributes to cover and to which extent. In addition, we reflect on the suitability of DCR Graphs as a tool for modelling an Internet of Things system since they have not been applied for this purpose previously. We also address the limitations of the DCR Tool, the graphical web-based interface used for constructing DCR Graphs encountered during the thesis work.