CSMOP: A Runtime Verification Tool For C# Programs
Runtime verification is a technique for evaluating the adherence of a program’s execution to a set of specifications. It is both more lightweight than other formal methods and more robust than unit testing, making it a promising candidate for industry use. There has been a considerable amount of research over the years on how to make runtime verification as efficient and useful as possible, but there is currently no developer-centric tool to help perform runtime verification on C# programs. In this thesis, we present CSMOP, a tool which addresses this need, targeting .NET 8 systems. CSMOP uses instrumentation to find relevant events as they occur at runtime, and takes a monitor-oriented approach to verifying the given sequence of events. Through JSON files, it accepts specifications written in one of three logical formalisms: finite state machine, linear temporal logic, and extended regular expressions. Upon program termination, CSMOP reports all violations of the specifications which occurred, along with the location where the violation happened. It uses modern algorithms in its monitors, monitor management, and paramatrization. It scales efficiently in terms of the number of encountered events and parameters. CSMOP includes a default set of specifications for the C# standard library, but can be easily extended for custom specifications.