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

•可修編.•可修編.安全软件理论与软硬件协同披it可打性研究报告一、 项目定义顶目名称安全软件理论与软硬件协同设廿顶目领域本项目属于基础产业和髙新技术领域，涝及廿算机软件与理论，系统芯片设itKit算机应用等学科。二、 贝目背景1.项目背景软件可靠性一直是廿算机界关心的关建课II,1967年欧洲软件工程先驱者Floyd提出用曲纳斷言法来验证程序的正确性;1969年图灵奖获得者Hoare提出使用程序公理系统来验证程序的性质。七十年代的典型程序语言的数学理论并不浅汝程序的规说明，因此不能用于软件的设计和开发。同时期的工作包括着重于程序性质的后验证的方法，被用于一些常用算法的分析与正确性证明，但缺之支持规分析和梧导安全软件设廿的演算技术。长期以来国际上不少软件公司投人了大量的人力、物力和财力探索软件设廿可靠性技术。设廿严格安全软件系统需要解决下述二顶关键技术间题：•建立程序和软件规的演算系貌，在軟件开发生命周期各阶段均使用数学演算技术来建立软件设廿和开发文档。•设廿完整的演算法则用来指导下述关建开发任务：从用户需求导出软件系统各部件的规说明；从部件的规说明演算出低层软件模挟过程的功能说明。在软件设廿中用数学理论来指导严格安全软件系统设廿,色括：•同一数学框架中处理程序和軟件规；•用符号演算实现程序和软件规间的演算;•用谓词演算验证设廿方法的正确性；•用代数方法从软件部件的抽象规说明推算出低层次程序模块各个过程的规说明。学科负责人自1985年起对设廿严格安全软件的完备演算理论进行了深人研究，取得了重大突破。主要仰新点有：•演算理论强调了设廿正确软件的开发方法和使用数学演算来支持从软件到程序代码的转换;•首先提出程序分解算武并第一次提出了求解规方程的演算法«;•首次给出程序设廿语言的一套完备的代数定律；•首先给出并证明由抽象数掘类型产生具体数据类型的完备演算法则;•首次为海量并行程序语言BSP培言建立指称培义和代数转化方法。主要学术成果fiS：•首次建立规的数学模型，并发现求解规方程（X;Q）＞S和（P；X）＞S的演算法则;•创建基于“上下仿真映照对”数据精化完备理论;•皿建程序代数（He-Hoa「e代数）,并用它来支持编译器原型的设廿和证明；•提出编程貌一理论和连接各类程序理论的数学法册。軟件演算理论和数据精化观呱被誉为是面向模型软件开发的一个里程碑，是国师标准规语言Z的精化理论基础，是欧洲系貌设计语言B的软件开发方法的理论及基碣。学科负责人还参・了包扌舌欧共体"便件编译器”顶目在的若干国际项目的研究，在前面理论工作的基础上，提出了“软硬件混合廿算系统"这一研究方向，同时，在KiOJ立了协同设廿研究方向，是1996年协同设廿程序委员会主席。这里提出的怵同设廿系貌与原先的设廿方法不同，如高速鉄路的硬件控制系统，可采用可编程器件，应用软件方法开发一f髙速挟路的控制系貌模型，看是否达到要求。若不行，只要修改所开发的软件（可由软件描述直接产生硕件的线路图），直到设廿出一个满意的模型化的髙速鉄胳，再实师生产。另外，象西门子公司的自动读电表的便件控制系貌，汽车上的导航控制系统，洗衣机自动控制的芯片等硬件系统的特点是:要使硬件价榕便宜，设廿时间短，乂要保证硬件设it系貌准确无误,这导致原先的设计方法很难满足这种要求。事实上，尺管已有若干工作，但迄今为止，软更件混合系统的分析和设廿是一f困难的课题，这是规代控制系貌的复杂性和可用苗片发展速度的局眼导致的。目前常用舸5!件描写语言（例如VHDL和VERILOG）允许设廿者在抽象设廿的不同层次间进行自由的混合,在低层设廿方面,如：基本电路（例:晶依管、门电路、寄存器）分层的、结构化的网链；在髙层设廿方面，io：设廿操作的行为表达。但实际上缺乏行为语旬。多数设廿方法依顿于仿真器的支持，设廿中的间题通过务次使用仿真程序来发规，因而开发周期和产品的可靠性那受到了很大的眼制。近年来也有应用廿算逻辑方法来验证徹处理器的正确性的尝试，包括髙阶逍辑验证工貝H0L、函数编程和抽象状态机等技术。然而此类形式的技术不能用来替代传统的仿真技术。目前急切需要的是一个基于形式化方法的设廿技术，色括使用仿真枝术来支持整个设廿的可视化和开发过程。形式化的法呱可以让硬件工程师来选择各类设廿参数和细节结构，而最后产品的依系结构仍然由工程设廿人员来确定。有关想法还被应用到各种廿算例中（例:用OCCAM写的程序和硕件的撤代码），同时CSP理论得到了充分的发展，提供了自动工具（OCCAM转换系统）。该系统被用TT800浮点单元的开发中，使T800提前一年完成。在工业界，模折很大程度上被汰为与验证是同义舸，设廿过程经常遵循由规得到实现的过程，二者可通过一系列的输人来进行模01,模拥可以重复进行，这样，錯娱之处將得以发规、改正。1993年至1996年,学科负贯人与Intel公司硬件验证小组和Cornell大学合作，设廿了-个硬件编译器。这类温语言的特征是：(1)对通过同步信息传送的并行进程、通那作了明确的描述；(2)非常自然地描述数字系统。这个顶目展示了怎样使用“握手模式的规”来为延时不敏感电路和时押电路产生一套等价的规格说明。一个自动工具被用于检査“低层的实现是否符合了它们的规”。该研究结果表明，应着重考虑在一f给定的系貌中建立欄念间的联系，这种联系在于:M态图(用来描术基本电路的行为);(b)延时不撤感代数(Delay-InsensitiveAlebraic)(用来详细说明延时不敏感电路)；(c)通讯序列进程(用来描述通讯界面);(d)时押进程代数(用来描述同步电路)；⑻控制和数据界面(用来將控制模式和数据模式联系起来)间的关系，这清楚地说明了要一个貌一构架来处理不同式、榔念间的界面的迫切性。过去几年里，学科负责人在撤处理器验证方面也作了一些成功的工作,有些工作采用HOL(fiDHighOrderLogic)系统，有些工作以“功能演算”和“抽象狀态机"为基础,不管怎样，形式化方法始终不能替代已有的模拥方法。所需要的_种方法，是使设计过程能以形式化技术为基础，但所包含的模扔过程能使设廿形象化，有助于系貌的开发。形武化的规呱被引用进来，能帮Bl硕件工程师更正确地it算参数,考虑设计细节，为工程判斷上的决策提供方法。这种将形式语义和可验证的模折器组合起来的方法將为工程设廿带来更髙的可靠性。解决仿真与合成的不一致性是关键间题。在软硬件混合系貌设廿的不同阶段所使用的系统语言是不同的。在需求分析阶段，时段逻辑语言和通讯进程代魏会用来描写系统的实时性质以及它和周边环境的交互功能。设廿阶段会使用一个并行语言来实现需求阶段所提出的函数和非函数功能，高级分解器会將这样一个程序自动分解为软件子系统和硬件子系统的描写，机器语言和网表语言Q是软件编译器和硬件综合器的目标语言。为了保证设廿方法的正确性，设廿过程被用到的务类语言就必须在同一语义框架中）111以形式化处理。这也被用来保证多类转换器（软硬件分析器,硬件综合器,软件编译器）设廿的正确牲。为了支持产品的优化设廿,协同设廿方法还得提供一套精化法呱用来实现语义等价设廿之间的转换，并基于代魏语义进行等价性证明。在此基础上，说明仿真器的工作与形式化描述的一致性。上述这些使得系统设廿可逐步引人多类优化来碱少物理资源的共享和控制逻辑的切換。同时,工具也是必需的。怵同设廿技术所使用的多类支持工貝ais：系统性能分林工具、系统分解器、交互式仿真器等。这里的主要挑战是设廿一个软便件混成系统的统一语义框架用来处理、验证多类转换系统的正确tto]i是基于培义等价变换设廿方法的数学基础，也是构造多类工具的逻辑基础。由于在混成型系貌设计各个阶段设廿人员会使用各种不同规、编程和设it语言与武，而多种文档之同的转换艮依赖于培义等价转换软件,为这一大类语言设廿共同的语义模里就成为整个设廿方法的关键难点。为了械少模型的复杂性，设it方法也得建立不同的语言之间的连接技术和变换法般。语义等价性间题是必须讨论和解决的。在软硬件混成系貌中，硕件的并行机制是建立在共享变量和信号呃动之上的，但软硬件之间的交互依赖于同步通讯机制。这种统一的语义框架就不得不浅及一个面向通讯和状态共享的混合型并行语言。这是在国际上还未研究过的难题。便件设廿语言VERILOG包含乡类在软件编程语言中从未使用过的结构和语句，它们的形式化描述和相应的精化法呱被国际廿算机界认为是对传统语义研究的一个挑战。为了增加该工具的灵活性,除了进行多类性能分林之外,还包括与用户直接交互的通讯手段，这也®jjut该软件工具设廿和实施的复杂性。还有一个技术难点涉及到软硬件子系鋭之间的通讯界面的设it,采用传统方法(同步或异步)使该部件结构规化，但会影喑整个混威系貌的性能，并且不利干系统的单茹片实现方案。为了塔加系统的安全性和可杨植性，本项目实施技术將不固定软硕件通讯界面的协议，而根据用户对系貌的要求(处理速度、信息量)来设廿面向应用的专用通讯界面。在系统的单茹片实施方案中，界面描写最终們可用硕件来实现。在设廿实时嵌人武系统中，由于可用的硬件资滌眼制(性能、助耗、面枳)，产品的优化是一个重要课题。软硬件转換器和分解器设廿中將结合多类分析优化技术来减少元器件的数目，增加元器件在硬件子系统中的重用性。将对应的结构重组(Reconfigurable)也是-个技术难点。將为软硬件混合系统的可组合描写、分林和设廿提供一个综合性的理论框架和设廿方法，它们具有下属几个特征:它能处理多类函数和非函数的需求分析,提出模块化和优化的处理方案。基于形武化技术，从而保证目标产品的可靠性和安全性。能容纳多类不同开发培言,并提供它们之间语义等价转换的法则。与硬件系统设计密切联系的软件方面，规格说明的形式化及相应的开发方法和验证工貝还未设廿出来。更进一步讲，许多现有的形式化方法缺乏足筋的应用围，它们没有将许多性质(如:可靠性、安全性)进行组合考虑。软硬件混合系统关鍵挑战是:为硬件、软件的协同设计寻找一个貌一构架，使我们的设廿能眼上“半导体设备及相应软件”复杂性的飞速増加。另外,也要求我们在这相同的构架，既要解决模拥与数字设备，同时也要解决多时押系统间题。准备采用IntervalTemporalLogic(iITL)作为高层规的描述工具,与其它逻辑不同，ITL既能用来描述顺序系统，Q能用来描述并行系貌，同时ITLQ强有力地支持工业界应用系统的安全性、实时性、可靠性等性质。由于模扔方法丈花时间，最终不能绝对保证硬件设廿的准确性。而向实际工业界应用的硬件系统，首先要保证准确，同时艮要提高开发速度,所以要研究面向“这些工业系统"硬件设it的软件开发方法，“硬件规"用ITL来描述，使设廿的准确性!0约到上述ITL公式的准确性。用本学科研究提供的软、硬件混合设廿方法，对于硬件系统的设廿而言,只要写出相应的软件描述即可。学科负责人在英国工作期间已经將这类方法使用在SONY公司的VCD稳定器和西敏寺银行的智能卡设it±o前者产品成本不到一美元,后者得到了英国工贸部LEVEL-5产品安全证书（最髙可靠性）。无论严格安全软件理论还是廿算机软班件协同设廿，均站在国际前列。三、顶目建按目标在严格安全软件理论与数据精化法则方面:貝备国际级影响；形成与欧美相当水平的学派;培养出一个良好的学术梯臥；并推出廿算机软硬件加同设计平台，为SOC（SystemOnChip）的设廿提供先进的开发工貝。这將是典型的具有原皿性和自主知识产权的产、学、研密切结合的标志性成果。我国SOC能力十分薄弱，在汽车、航天、家电、医疗行业和金融界等，这样的平台有着极为广泛的应用前景。现在，我国研究人员往往去西方发达学习、诉间。建议重点学科若被批准，相信国外的研究人员将到这里来学习、诉间。四、項目建按所需经贵本项目建设总投入经费900JJ元，其中中央专项资金1OOJJ元（即廿委100H元)，XX市政府配套100开元，学校自筹资金(学校教育产业及事业收费收人等)700开元。具体资金投向为：设备与坏境730牙元；国际学术活动70JJ元;学科建设资料100JT元。本顶目抑购的代表性仪器设备有：SUN服务器、主要用于怵同廿算的IBM主机、用于科学计算的IBM小型机等。五、项目建按巳有条件、优势和特点学科所在的软件学院是35所软件学院之一，学校、