.安全软件理论与软硬件协同设计可行性研究报告一、项目定义1. 项目名称安全软件理论与软硬件协同设计2. 项目领域本项目属于基础产业和高新技术领域，涉及计算机软件与理论， 系统芯片设计及计算机应用等学科。二、项目背景1项目背景软件可靠性一直是计算机界关心的关键课题， 1967 年欧洲软件工程先驱者 Floyd 提出用归纳断言法来验证程序的正确性； 1969 年图灵奖获得者 Hoare 提出使用程序公理系统来验证程序的性质。七十年代的典型程序语言的数学理论并不涉及程序的规范说明， 因此不能用于软件的设计和开发。 同时期的工作包括着重于程序性质的后验证的方法， 被用于一些常用算法的分析与正确性证明，但缺乏支持规范分析和指导安全软件设计的演算技术。长期以来国际上不少软件公司投入了大量的人力、物力和财力探索软件设计可靠性技术。设计严格安全软件系统需要解决下述二项关键技术问题: 建立程序和软件规范的演算系统，在软件开发生命周期各阶段均使用数学演算技术来建立软件设计和开发文档。
