A Flexible Framework for Supporting Multi-language Simulation and Verification

[[abstract]]Multi-threading and multi-core technology introduce more computing power to software system, but unfortunately, concurrency makes system correctness more difficult to verify. To many critical systems, failures could cost lives and large amount of money, so the correctness plays a vital role in the development of such systems. In recent years, model checking is the most popular approach to address the problem. Model checking often requires users to abstract a model from a target system. But the abstraction process between source code and model often drives programmers away from such technique. This explains why verification tools are still far from practical usage. Having users write model with high-level programming language is the most straightforward idea to ease the use of verification tools. Nevertheless, the cost of building and maintaining a programming language parser and its related components is high. In this thesis, we propose an intermediate data structure based on control flow graph. In the future, we expect the input program will be translated into such control flow graph. The control flow graph serves as the standard representation for our backend analysis engine. ArCats (Architecture Refactoring and Concurrency Analysis Tool Suite) is a research prototype this work is built from. It runs in the two different graph-like data structure, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), by polymorphism technique in OOP. In the compositional analysis module, we use CCS as model input. In this thesis, the component that translates the revised CFG to CCS is also described.