Sustainable social development and quality assurance of software systems to manage

Control software is intensively used for decision making in critical spheres of the modern society, from technology process control to inboard control systems in avionic and space vehicles. Modern society life become more and more dependable from correctness of control software. In the paper there presented examples of software errors and material losses and losses of human lives. Program verification results are discussed and a new promising approach to program verification called model checking is analyzed. Model checking is based on formal methods. It may considerably decrease the number of critical errors in control software.