工业控制系统的软件可信属性验证（1）

控制系统的软件可信属性验证（1）"/>

工业控制系统的软件可信属性验证（1）

对我这是一个全新的领域，先从国内的综述学起吧！！我会把需要进行后续延伸的内容和需要了解的内容记录下来。也会有自己的见解。

可信计算的研究与发展

可信计算是一种信息系统安全新技术，包括可信硬件、可信软件、可信网络和可信计算应用等诸多方面。

2007年，中国国家自然科学基金委员会启动“可信软件重大专项”支持可信软件的研究。

软件的可信性问题也日益突出，以高可信软件工程技术为重要内容的软件研究成为软件技术研究的热点之一[高可信软件工程技术]。所谓可信软件，通常是指在特定环境下其运行行为及其结果符合人们预期，并在受到干扰时仍能够提供连续服务的软件[可信软件期初研究重大研究计划综述]。

目前软件可信性验证的主要进展如下：

形式化方法在可信软件技术中有重要的应用与实践[formal methods: practiceand experience]。从理论框架上看，抽象解释理论是一个重要的方向[Abstract interpretationbased formal methods and future challenges]。从技术上看，软件分析以软件为对象通过静态或动态的方法进行人工或自动分析，以验证、确认、监控或发现软件性质（或者规约、约束），取得重要进展[软件分析技术进展]。例如，Coverity [www.coverity]、C Global Surveyor [precise andscalable static program analysis of NASA flight software]，ASTREE [a static analyzer for large safety-critical software]等静态分析工具能较好地分析程序中是否有运行时