安全软件理论与软硬件协同设计可行性研究应用报告.doc

安全软件理论和软硬件协同设计可行性研究汇报

一、项目定义
1．项目名称
安全软件理论和软硬件协同设计
2．项目领域
本项目属于基础产业和高新技术领域，包含计算机软件和理论，系统芯片设计及计算机应用等学科。

二、项目背景

1．项目背景
软件可靠性一直是计算机界关心关键课题，1967年欧洲软件工程先驱者Floyd提出用归纳断言法来验证程序正确性；1969年图灵奖取得者Hoare提出使用程序公理系统来验证程序性质。
七十年代经典程序语言数学理论并不包含程序规范说明，所以不能用于软件设计和开发。同时期工作包含着重于程序性质后验证方法，被用于部分常见算法分析和正确性证实，但缺乏支持规范分析和指导安全软件设计演算技术。
长久以来国际上不少软件企业投入了大量人力、物力和财力探索软件设计可靠性技术。
设计严格安全软件系统需要处理下述二项关键技术问题:
● 建立程序和软件规范演算系统，在软件开发生命周期各阶段均使用数学演算技术来建立软件设计和开发文档。
● 设计完整演算法则用来指导下述关键开发任务：
（a）从用户需求导出软件系统各部件规范说明；
（b）从部件规范说明演算出低层软件模块过程功效说明。
在软件设计中用数学理论来指导严格安全软件系统设计，包含：
● 同一数学框架中处理程序和软件规范；
● 用符号演算实现程序和软件规范间演算；
● 用谓词演算验证设计方法正确性；
● 用代数方法从软件部件抽象规范说明推算出低层次程序模块各个过程规范说明。
学科责任人自1985年起对设计严格安全软件完备演算理论进行了深入研究，取得了重大突破。关键创新点有：
● 演算理论强调了设计正确软件开发方法和使用数学演算来支持从软件到程序代码转换；
● 首先提出程序分解算式并第一次提出了求解规范方程演算法则；
● 首次给出程序设计语言一套完备代数定律；
● 首先给出并证实由抽象数据类型产生具体数据类型完备演算法则；
● 首次为海量并行程序语言BSP语言建立指称语义和代数转化方法。
关键学术结果包含：
● 首次建立规范数学模型，并发觉求解规范方程(X;Q)>S 和 (P;X)>S 演算法则；
● 创建基于“上下仿真映照对”数据精化完备理论；
● 创建程序代数(He-Hoare代数)，并用它来支持编译器原型设计和证实；
● 提出编程统一理论和连接各类程序理论数学法则。
软件演算理论和数据精化规则被誉为是面向模型软件开发一个里程碑，是国际标准规范语言Z精化理论基础，是欧洲系统设计语言B软件开发方法理论及基础。
学科责任人还参与了包含欧共体“硬件编译器”项目在内若干国际项目标研究，在前面理论工作基础上，提出了“软硬件混累计算系统”这一研究方向，同时，在欧洲创建了协同设计研究方向，是1996年协同设计程序委员会主席。
这里提出协同设计系统和原先设计方法不一样，如高速铁路硬件控制系统，可采取可编程器件，应用软件方法开发一个高速铁路控制系统模型，看是否达成要求。若不行，只要修改所开发软件(可由软件描述直接产生硬件线路图)，直到设计出一个满意模型化高速铁路，再实际生产。另外，象西门子企业自动读电表硬件控制系统，汽车上导航控制系统，洗衣机自动控制芯片等硬件系统特点是：要使硬件价格廉价，设计时间短，又要确保硬件设计系统正确无误，这造成原先设计方法极难满足这种要求。
实际上，尽管已经有若干工作，但迄今为止，软硬件混合系统分析和设计是一个困难课题，这是现代控制系统复杂性和可用芯片发展速度局限造成。现在常见硬件描写语言（比如VHDL和VERILOG）许可设计者在抽象设计不一样层次间进行自由混合，在低层设计方面，如：基础电路(例：晶体管、门电路、寄存器)分层、结构化网链；在高层设计方面，如：设计操作行为表示。但实际上缺乏行为语句。多数设计方法依靠于仿真器支持，设计中问题经过数次使用仿真程序来发觉，所以开发周期和产品可靠性全部受到了很大限制。多年来也有应用计算逻辑方法来验证微处理器正确性尝试，包含高阶逻辑验证工具HOL、函数编程和抽象状态机等技术。然而这类形式技术不能用来替换传统仿真技术。现在急切需要是一个基于形式化方法设计技术，包含使用仿真技术来支持整个设计可视化和开发过程。形式化法则能够让硬件工程师来选择各类设计参数和细节结构，而最终产品体系结构仍然由工程设计人员来确定。
相关想法还被应用到多种计算范例中(例：用OCCAM写程序和硬件微代码)，同时CSP理论得到了充足发展，提供了自动工具(OCCAM转换系统)。该系统被用于T800浮点单元开发中，使T800提前十二个月完成。
在工业界，模拟很大程度上被认为和验证是同义，设计过程常常遵照由规范得到实现过程，二者可经过一系列输入来进行模拟，模拟能够反复进行，这么，错误之处将得以发觉、更正。
1993年至1996年，学科责任人和Intel企业硬件验证小组和Cornell大学合作，设计了一个硬件编译器。这类源语言特征是：(1)对经过同时信息传送并行进程、通讯作了明确描述；(2)很自然地描述数字系统。这个项目展示了怎样使用“握手模式规范”来为延时不敏感电路和时钟电路产生一套等价规格说明。一个自动工具被用于检验“低层实现是否符合了它们规范”。
该研究结果表明，应着重考虑在一个给定系统中建立概念间联络，这种联络在于：(a)状态图(用来描术基础电路行为)；(b)延时不敏感代数(Delay-Insensitive Alebraic)(用来具体说明延时不敏感电路)；(c)通讯序列进程(用来描述通讯界面)；(d)时钟进程代数(用来描述同时电路)；(e)控制和数据界面(用来将控制模式和数据模式联络起来)间关系，这清楚地说明了要一个统一构架来处理不一样范式、概念间界面迫切性。
过去几年里，学科责任人在微处理器验证方面也作了部分成功工作，有些工作采取HOL(即High Order Logic)系统，有些工作以“功效演算”和“抽象状态机”为基础，不管怎样，形式化方法一直不能替换已经有模拟方法。所需要一个方法，是使设计过程能以形式化技术为基础，但所包含模拟过程能使设计形象化，有利于系统开发。形式化规则被引用进来，能帮助硬件工程师更正确地计算参数，考虑设计细节，为工程判定上决议提供方法。这种将形式语义和可验证模拟器组合起来方法将为工程设计带来更高可靠性。处理仿真和合成不一致性是关键问题。
在软硬件混合系统设计不一样阶段所使用系统语言是不一样。在需求分析阶段，时段逻辑语言和通讯进程代数会用来描写系统实时性质和它和周围环境交互功效。设计阶段会使用一个并行语言来实现需求阶段所提出函数和非函数功效，高级分解器会将这么一个程序自动分解为软件子系统和硬件子系统描写，机器语言和网表语言又是软件编译器和硬件综合器目口号言。为了确保设计方法正确性，设计过程被用到多类语言就必需在同一语义框架中加以形式化处理。这也被用来确保多类转换器(软硬件分析器，硬件综合器，软件编译器)设计正确性。为了支持产品优化设计，协同设计方法还得提供一套精化法则用来实现语义等价设计之间转换，并基于代数语义进行等价性证实。在此基础上，说明仿真器工作和形式化描述一致性。
上述这些使得系统设计可逐步引入多类优化来降低物理资源共享和控制逻辑切换。同时，工具也是必需。协同设计技术所使用多类支持工具包含：系统性能分析工具、系统分解器、交互式仿真器等。
这里关键挑战是设计一个软硬件混成系统统一语义框架用来处理、验证多类转换系统正确性。这是基于语义等价变换设计方法数学基础，也是结构多类工具逻辑基础。因为在混成型系统设计各个阶段设计人员会使用多种不一样规范、编程和设计语言和范式，而多个文档之间转换又依靠于语义等价转换软件，为这一大类语言设计共同语义模型就成为整个设计方法关键难点。为了降低模型复杂性，设计方法也得建立不一样语言之间连接技术和变换法则。语义等价性问题是必需讨论和处理。
在软硬件混成系统中，硬件并行机制是建立在共享变量和信号驱动之上，但软硬件之间交互依靠于同时通讯机制。这种统一语义框架就不得不包含一个面向通讯和状态共享混合型并行语言。这是在国际上还未研究过难题。硬件设计语言VERILOG包含多类在软件编程语言中从未使用过结构和语句，它们形式化描述和对应精化法则被国际计算机界认为是对传统语义研究一个挑战。为了增加该工具灵活性，除了进行多类性能分析之外，还包含和用户直接交互通讯手段，这也增加了该软件工具设计和实施复杂性。
还有一个技术难点包含到软硬件子系统之间通讯界面设计，采取传统方法（同时或异步）使该部件结构规范化，但会影响整个混成系统性能，而且不利于系统单芯片实现方案。为了增加系统安全性和可移植性，本项目实施技术将不固定软硬件通讯界面协议，而依据用户对系统要求（处理速度、信息量）来设计面向应用专用通讯界面。在系统单芯片实施方案中，界面描写最终仍可用硬件来实现。在设计实时嵌入式系统中，因为可用硬件资源限制（性能、功耗、面积），产品优化是一个关键课题。软硬件转换器和分解器设计中将结合多类分析优化技术来降低元器件数目，增加元器件在硬件子系统中重用性。将对应结构重组（Reconfigurable）也是一个技术难点。
将为软硬件混合系统可组合描写、分析和设计提供一个综合性理论框架和设计方法，它们含有下属多个特征：
（1）它能处理多类函数和非函数需求分析，提出模块化和优化处理方案。
（2）基于形式化技术，从而确保目标产品可靠性和安全性。
（3）能容纳多类不一样开发语言，并提供它们之间语义等价转换法则。
和硬件系统设计亲密联络软件方面，规格说明形式化及对应开发方法和验证工具还未设计出来。更深入讲，很多现有形式化方法缺乏足够应用范围，它们没有将很多性质(如：可靠性、安全性)进行组合考虑。软硬件混合系统关键挑战是：为硬件、软件协同设计寻求一个统一构架，使我们设计能跟上“半导体设备及对应软件”复杂性飞速增加。另外，也要求我们在这相同构架内，既要处理模拟和数字设备，同时也要处理多时钟系统问题。
准备采取Interval Temporal Logic(即ITL)作为高层规范描述工具，和其它逻辑不一样，ITL既能用来描述次序系统，又能用来描述并行系统，同时ITL又强有力地支持工业界应用系统安全性、实时性、可靠性等性质。因为模拟方法太花时间，最终不能绝对确保硬件设计正确性。而向实际工业界应用硬件系统，首先要确保正确，同时又要提升开发速度，所以要研究面向“这些工业系统”硬件设计软件开发方法，“硬件规范”用ITL来描述，使设计正确性归约到上述ITL公式正确性。
用本学科研究提供软、硬件混合设计方法，对于硬件系统设计而言，只要写出对应软件描述即可。
学科责任人在英国工作期间已经将这类方法使用在SONY企业VCD稳定器和西敏寺银行智能卡设计上。前者产品成本不到一美元，后者得到了英国工贸部LEVEL-5产品安全证书（最高可靠性）。
不管严格安全软件理论还是计算机软硬件协同设计，均站在国际前列。

三、项目建设目标

在严格安全软件理论和数据精化法则方面：
含有国际级影响；
形成和欧美相当水平学派；
培养出一个良好学术梯队；
并推出计算机软硬件协同设计平台，为SOC(System On Chip)设计提供优异开发工具。这将是经典含有原创性和自主知识产权产、学、研亲密结合标志性结果。
中国SOC能力十分微弱，在汽车、航天、家电、医疗行业和金融界等，这么平台有着极为广泛应用前景。
现在，中国研究人员往往去西方发达国家学习、访问。提议关键学科若被同意，相信国外研究人员将到这里来学习、访问。

四、项目建设所需经费

本项目建设总投入经费900万元，其中中央专题资金100万元（即国家计委100万元），上海市政府配套100万元，学校自筹资金（学校教育产业及事业收费收入等）700万元。
具体资金投向为：设备和环境730万元；国际学术活动70万元；学科建设资料100万元。
本项目拟购代表性仪器设备有：SUN服务器、关键用于协同计算IBM主机、用于科学计算IBM小型机等。

五、项目建设已经有条件、优势和特点

学科所在软件学院是国家35所软件学院之一，学校、复星高科技集团、国家外国教授局和海外银行在政策和财力方面给了多种支持。国家软件人才国际培训（上海）基地，是江、浙、沪唯一这类基地。原有“计算机软件和理论”、“计算机应用”和“系统分析和集成”等点是学科发展依靠。
6月27日，国务院下发了《激励软件产业和集成电路产业发展若干政策》，可见软件产业和集成电路产业之关键。计算机软硬件协同设计系统是面向集成电路设计、尤其是系统芯片（System on Chip, SOC）设计软件开发平台，它直接包含了软件和集成电路设计这两个信息产业支柱，又是产、学、研亲密结合产品。