Editorial

摘要

Runtime verification is a recent direction in formal methods research; it is complementary to well-established formal verification methods, such as model checking. Research in runtime verification deals with formal languages suitable for expressing system properties that are checkable at run time, algorithms for the checking of formal properties over an execution trace, and low-overhead means of extracting information from the running system that is sufficient for checking of the property. Applications of runtime verification technology include: post-deployment monitoring of system correctness and performance, construction of formally specified test oracles, and collection of statistics about system behaviour, among others.