An approach to formal verification of embedded software

Abstract

Modern distributed large-scale systems comprise very large number of embedded processors, which are running embedded software. The complexity of these systems of systems is so high that it becomes unmanageable by humans. Under such circumstances, formal methods and the corresponding tools is being a subject of intensive research and development in both industry and academia. The objective of this paper is to make a contribution to the overall efforts by proposing a method, and accompanying tools, for formal verification of a class of embedded software that may be modeled as a collection of distributed finite state machines. The method is based on the symbolic model verification of certain properties of embedded software models. The accompanying tools enable creation of these models from the high-level design models and/or from the target program code, e.g. in C/C++ language. The viability of the proposed method is demonstrated on a case study. The subject of the case study is the verification of distributed embedded software that executes in the telephone switches and call centers. The results of the case study show that the proposed method is applicable on the real-world systems.