Open AccessGeneric Methodology for Formal Verification of UML Models
Author(s) -
K.H. Kochaleema,
G. Santhosh Kumar
Publication year - 2022
Publication title -
defence science journal/defence science journal
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.198
H-Index - 32
eISSN - 0976-464X
pISSN - 0011-748X
DOI - 10.14429/dsj.72.17228
Subject(s) - computer science , applications of uml , correctness , unified modeling language , uml tool , programming language , formal methods , model checking , formal verification , computation tree logic , systems modeling language , object constraint language , software engineering , software
This paper discusses a Unified Modelling Language (UML) based formal verification methodology for early error detection in the model-based software development cycle. Our approach proposes a UML-based formal verification process utilising functional and behavioural modelling artifacts of UML. It reinforces these artifacts with formal model transition and property verification. The main contribution is a UML to Labelled Transition System (LTS) Translator application that automatically converts UML Statecharts to formal models. Property specifications are derived from system requirements and corresponding Computational Tree Logic (CTL)/Linear Temporal Logic (LTL) model checking procedure verifies property entailment in LTS. With its ability to verify CTL and LTL specifications, the methodology becomes generic for verifying all types of embedded system behaviours. The steep learning curve associated with formal methods is avoided through the automatic formal model generation and thus reduces the reluctance of using formal methods in software development projects. A case study of an embedded controller used in military applications validates the methodology. It establishes how the methodology finds its use in verifying the correctness and consistency of UML models before implementation.