Methodology for Integrating Computational Tree Logic Model Checking in Unified Modelling Language Artefacts: A Case Study of an Embedded Controller

摘要

A unified modelling language (UML) based formal verification methodology that can be easily integrated into an embedded system software development life cycle is suggested. The approach augments UML diagrams with formal models through an interfacing domain and adds semantics to these diagrams. The suggested methodology; commences from functional specification and use case modelling, selects the most critical behaviour where formal verification can add value to the development cycle, analyses the selected behaviour using UML state transition diagram, derives a state chart matrix from the same, and a high level language software translates the state chart matrix to a labelled transition system. Safety properties are derived from system specifications and are expressed as computation tree logic (CTL) formulae. CTL model-checking algorithm from the literature is used for model-checking. The applicability of the suggested approach is established using a safety critical embedded controller used for deployment and recovery of sensor structures from an airborne platform.