The paper analyzes the existing problems of software engineering, due to the complexity of modern programs and parallel execution of cooperating processes. A review of formal methods for the design and verification, allowing proving the conformity of program models and system’s formal requirements, was performed. The features of the method of formal verification Model Checking and its development for the verification of UML state-charts were reviewed. The syntax and semantics of temporal logic μUCTL and formal representation UML models, as doubly labeled systems (L2TS), were investigated.
programming, formal methods, verification, Model Checking, UML
"Metod formalnoi veryfykatsyy UMC: UML Model Checking" ,
Information Processing Systems,