Generic Methodology for Formal Verification of UML Models

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.

Download Full-text

Monitoring and Testing Based on Multi-Level Program Specifications

Proceedings of the Institute for System Programming of RAS ◽

10.15514/ispras-2020-32(6)-1 ◽

2020 ◽

Vol 32 (6) ◽

pp. 7-18

Author(s):

Alexander Konstantinovich Petrenko ◽

Denis Valentinovich Efremov ◽

Eugeny Valerievich Kornykhin ◽

Alexey Vladimirovich Khoroshilov ◽

Ilya Viktorovich Shchepetkov ◽

...

Keyword(s):

Software Development ◽

Formal Verification ◽

Formal Methods ◽

Software Systems ◽

Iterative Development ◽

Multi Level ◽

Large Software ◽

Implementation Level

Research on formal methods of software development and verification focuses on building specifications using incremental and iterative development methodologies. The presence of several levels of specifications simplifies proving of properties, since it is possible to reuse the proofs that were performed for more abstract layers of the model. It is desirable to use the same models that were used for formal verification also in testing of real systems for compliance with the requirements set by these models. In practice, large software systems are described by multi-level models. There was no experience of using such models as the basis for testing and monitoring. The paper discusses various methods for developing multi-level models, new opportunities that can be obtained through a combination of functional specifications and implementation-level refinements, limitations that must be considered during testing and monitoring of real systems for compliance with multi-level models.

Download Full-text

The Role of Formal Methods in Software Development for Railway Applications

Software Design and Development ◽

10.4018/978-1-4666-4301-7.ch054 ◽

2014 ◽

pp. 1103-1118

Author(s):

Alessandro Fantechi

Keyword(s):

Model Checking ◽

Software Development ◽

Formal Verification ◽

Formal Methods ◽

Industrial Application ◽

Safety Certification ◽

Software Designers ◽

Recent Trends ◽

Railway Domain

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.

Download Full-text