CSHARPTOUPPAAL: A ROSLYN-BASED STATIC TRANSLATOR FROM GENERAL-PURPOSE C# PROGRAMS TO UPPAAL TIMED-AUTOMATA NETWORKS

Abstract

A lot of C# code is written like this: approval flows, protocol handlers, controller actions, etc. - that is, in a very simple logic structure that looks like a state machine. It is almost never formally model.checked, as this would necessitate the creation by hand of the equivalent UPPAAL timed-automata model, which is slow, error prone and not scalable beyond toy examples. This paper introduces a tool called CSharpToUppaal that statically translates a C# program, a folder of programs, or a complete MSBuild project or solution, into a network of timed-automata in the UPPAAL 4.1 framework. There are four aspects of the design that set the tool apart from a standard control-flow-to-automaton mapper. All the methods included will be turned into their own UPPAAL template, with synchronisation channels between them instead of inline or native UPPAAL functions. A heuristic for choosing which functions to model during the walk is implemented, allowing the user to not hand-pick every single one, by walking the call graph. Methods that are not callable from calls become bounded nondeterministic stubs, not silent gaps, and the user is required to confirm that they can be exported. and a static validator is used to check for the structural well-formedness of the generated UPPAAL XML and prevent export if it is not well-formed. The translation rules for sequencing, branching, looping, return and inter-procedural calls are described in sufficient detail to verify them against the implementation, and the reason why recursive call graphs are not accepted but instead are rejected outright, is explained. The paper assesses the tool along three axes with real results: the existing test suite, 50 tests which succeed with the tool, across two assemblies with no failures; every generated template across those five fixtures lays out with zero edge crossings; and a self-audit of the scope-inference heuristic against the tool's own 114-function GUI codebase selects a 15.8% closure, as well as surfaceing UI-plumbing functions the heuristic probably should have excluded. We are honest in what the tool can (and cannot) support: CSharpToUppaal generates structurally correct and traceable models that have explicit and inspectable assumptions. It does not, produce a verified-equivalent or fully automatic formal model of the source program. Our contributions in this paper are related to keywords such as model checking, UPPAAL, timed automata, static analysis, Roslyn, C#, program translation, formal verification, and tool paper.