Formal Verification of Embedded Software Based on Software Compliance Properties and Explicit Use of Time
The complexity of embedded software running in modern distributed large-scale systems is going so high that it becomes hardly manageable by humans. Formal methods and the supporting tools are offering effective means for mastering complexity, and therefore they are remaining to be an important subject of intensive research and development in both industry and academia. This paper makes a contribution to the overall R&D efforts in the area by proposing a method, and supporting tools, for formal verification of a class of embedded software, which may be modeled as a collection of distributed finite state machines. The method is based on the model checking of certain properties of embedded software models by cadence SMV tool.