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