一种基于System C语言的模型检测方法

A Method of Model Checking based on System C

System C语言在软硬件协同设计过程中被广泛用来建模和仿真.笔者提出了一种验证System C设计的方法,即通过把System C设计映射成为一个具有良好定义语义的UPPAAL时间自动机.System C设计的结构和非正式定义的行为在形成的UPPAAL时间自动机中得到了完整的保留.产生的UPPAAL模型允许使用UPPAAL模型检查器和其配套工具来进行验证.模型检查器用来验证设计的一些重要属性,比如活性,死锁问题和时间约束属性.通过对两个实例的活性、安全性和时间属性的验证来证明该方法的适用性.

System C is widely used for modeling and simulation in hardware/software co-design. Due to the lack of a complete formal semantics, it is not possible to verify System C designs. In this paper, we present an approach to overcome this problem by defining the semantics of System C by a mapping from System C designs into the well-defined semantics of UPPAAL timed automata. The informally defined behavior and the structure of System C designs are completely preserved in the generated UPPAAL models. The resuiting UPPAAL models allow us to use the UPPAAL model checker and the UPPAAL tool suite, including simulation and visualization tools. The model checker can be used to verify important properties such as live- ness, deadlock freedom or compliance with timing constraints. We have implemented the presented transformation, applied it to two examples and verified liveness, safety and timing properties by model checking, thus showing the applicability of our approach in practice.