JOINT APPLICATION OF CONTRACTS AND VERIFICATION FOR AUTOMATA-BASED PROGRAMS QUALITY ENHANCEMENT
Read the full article
Quality assurance is an important aspect of development of software systems with complex behavior. The price of error in such systems may be too high, so it is important not just to check all program specifications, but also to make the process efficient and automated as much as possible. In practice, it can be achieved by formalizing the program requirements and storing the executable specification directly with the program code. This paper presents the review of existing quality control methods applicable to software systems with complex behavior. The process of environment creation is described supporting three most common approaches to quality assurance of automata-based programs: model checking, unit testing, and contracts. The proposed approach helps to keep program specification up-to-date with availability of interactive quality control.