Correctness verification of concurrent systems
Tomasz Szmuc · 2003
Formal tools and computer support for correctness verification are proposed. An algebraic process description of the correctness facilitates formal tools aiding correctness proving. Two methods of correctness verification are presented: static verification, corresponding to the verification notion in system programming which is informally described by the software standard; and dynamic correction, which is a generalization of the exception-handling idea. Algorithms for these methods are specified.>