Simulation with Compositional Analysis

[[abstract]]In recent years, compositional analysis in the automatic verification techniques is known as a promising approach. The states in subsystem can be minimized and hidden to alleviate state explosion while building the interface process that represents the whole subsystem. However, the key of success relies on a good modularity in system architecture. Some systems are still not amenable to compositional analysis. Simulation is an optimistic quality assurance like testing. Simulation can avoid exhausting memory while exploring state space. In the area of hardware validation, it is practical but cannot provide assurance in absence of errors. Given enough time, critical errors may still be manifested by simulation technique. In the paper, we combine simulation and compositional analysis together. Processes in a subsystem are composed into an interface process. Simulation that walks into the interface process is equal to walk a lot of hidden states in the subsystem. The simulator of ArCats runs in the two different graph, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), with polymorphism technique in OOP. The advantages of simulation with compositional analysis are shown by examples and evaluation.