Model Checking Approach to the Correctness Proof of Complex Systems
Marina Alekseeva, Ekaterina Dashkova · Proceedings of the Spring/Summer young researchers' colloquium on software engineering · 2011
Very often the question of efficiency in terms of execution time memory usage, or power consumption of the dedicated hardware/software systems is of utmost interest that is why different variants of algorithms are developed.In many situations the original algorithm is modified to improve its efficiency in terms like power consumption or memory consumption which were not in the focus of the original algorithm.For all this modifications it is crucial that functionality and correctness of the original algorithm is preserved [1].A lot of systems increasingly applying embedded software solutions to gain flexibility and cost-efficiency.One of the various approaches toward the correctness of systems is a formal verification technique which allows to verify the desirable behavior properties of a given system.This technique nowadays is well known as model checking.Model is expected to satisfy desirable properties.Verification is the analysis of properties of all admissible program results through formal evidence for the presence of required properties.The basic idea of verifying the program is to formally prove the correspondence between the programming language and the specification of the problem.Program and specification describe the same problem using different languages.Specification languages are purely declarative, human-centered.Imperative programming languages are more focused on executing on the computing device.Therefore less natural for men.Likewise, this technique is an excellent debugging instrument.From the standpoint of programming technology verification enables to obtain a better strategy for debugging programs.