基于Petri网的代码缺陷静态分析中的关键问题研究

程序缺陷由于直接或间接地非法使用了某些非授权的数据或者资源，或者合法地使用了某些非法的数据或者资源所导致。资源就是计算机系统具有的，数据通过物理资源实施并被观察的。因此，程序缺陷涉及两个域，一个是抽象的算法（数学上的缺陷）；一个是计算机系统的物理资源的访问。因此，程序是算法和实施算法的物理资源分配的一种描述。当算法和物理资源合一时，不仅语义可能发生变化，而且缺陷也会产生。如果程序形式规范中描述了程序中涉及到的计算机平台的资源，就可以极大地缩减并定位缺陷产生的原因和范围。本项目对程序从计算语义和物理实现语义两个方面进行建模，研究程序中数据、控制以及资源之间的关系。在代码和形式规范两个层面分析程序，获得程序的静态特征和动态行为，最终有效地发现用户所关心的属性。