Use of computers in controlling safety-critical and real-time systems is steadily increasing. Software safety is a critical concern in such systems where the potential worst-case consequences may include the loss of life, injury, grave harm to propery, or environmental damage.
An approach to the software safety problem is to model the proposed system behavior and perform safety analysis prior to the actual system development. In this thesis, we propose a safety analysis method using a high-level Petri Net formalism known as the Coloured Petri nets (CPN). CPN significantly extends the expressiveness of the classical Place-Transition nets(PTN) while preserving theoretical analyzability of the model.
Safety analysis methods often employ backward analysis, and PTN-based backward safety analysis method is straightforward and well-understood. However, increased expressiveness of CPN makes the task of software safety analysis more difficulty. Technical difficulties in adopting backward analysis using CPN are investigated, and a rigorous procedure to overcome the difficulties is presented.
