安全軟件理論與軟硬件協(xié)同設(shè)計(jì)可行性研究報(bào)告

安全軟件理論與軟硬件協(xié)同設(shè)計(jì)可行性研究報(bào)告一、項(xiàng)目定義1．項(xiàng)目名稱安全軟件理論與軟硬件協(xié)同設(shè)計(jì)2．項(xiàng)目領(lǐng)域本項(xiàng)目屬于基礎(chǔ)產(chǎn)業(yè)和高新技術(shù)領(lǐng)域，涉及計(jì)算機(jī)軟件與理論，系統(tǒng)芯片設(shè)計(jì)及計(jì)算機(jī)應(yīng)用等學(xué)科。二、項(xiàng)目背景1．項(xiàng)目背景軟件可靠性一直是計(jì)算機(jī)界關(guān)心的關(guān)鍵課題，1967年歐洲軟件工程先驅(qū)者Floyd提出用歸納斷言法來驗(yàn)證程序的正確性；1969年圖靈獎(jiǎng)獲得者Hoare提出使用程序公理系統(tǒng)來驗(yàn)證程序的性質(zhì)。七十年代的典型程序語言的數(shù)學(xué)理論并不涉及程序的規(guī)范說明，因此不能用于軟件的設(shè)計(jì)和開發(fā)。同時(shí)期的工作包括著重于程序性質(zhì)的后驗(yàn)證的方法，被用于一些常用算法的分析與正確性證明，但缺乏支持規(guī)范分析和指導(dǎo)安全軟件設(shè)計(jì)的演算技術(shù)。長期以來國際上不少軟件公司投入了大量的人力、物力和財(cái)力探索軟件設(shè)計(jì)可靠性技術(shù)。設(shè)計(jì)嚴(yán)格安全軟件系統(tǒng)需要解決下述二項(xiàng)關(guān)鍵技術(shù)問題:●建立程序和軟件規(guī)范的演算系統(tǒng)，在軟件開發(fā)生命周期各階段均使用數(shù)學(xué)演算技術(shù)來建立軟件設(shè)計(jì)和開發(fā)文檔。●設(shè)計(jì)完整的演算法則用來指導(dǎo)下述關(guān)鍵開發(fā)任務(wù)：（a）從用戶需求導(dǎo)出軟件系統(tǒng)各部件的規(guī)范說明；（b）從部件的規(guī)范說明演算出低層軟件模塊過程的功能說明。在軟件設(shè)計(jì)中用數(shù)學(xué)理論來指導(dǎo)嚴(yán)格安全軟件系統(tǒng)設(shè)計(jì)，包括：●同一數(shù)學(xué)框架中處理程序和軟件規(guī)范；●用符號(hào)演算實(shí)現(xiàn)程序和軟件規(guī)范間的演算；●用謂詞演算驗(yàn)證設(shè)計(jì)方法的正確性；●用代數(shù)方法從軟件部件的抽象規(guī)范說明推算出低層次程序模塊各個(gè)過程的規(guī)范說明。學(xué)科負(fù)責(zé)人自1985年起對(duì)設(shè)計(jì)嚴(yán)格安全軟件的完備演算理論進(jìn)行了深入研究，取得了重大突破。主要?jiǎng)?chuàng)新點(diǎn)有：●演算理論強(qiáng)調(diào)了設(shè)計(jì)正確軟件的開發(fā)方法和使用數(shù)學(xué)演算來支持從軟件到程序代碼的轉(zhuǎn)換；●首先提出程序分解算式并第一次提出了求解規(guī)范方程的演算法則；●首次給出程序設(shè)計(jì)語言的一套完備的代數(shù)定律；●首先給出并證明由抽象數(shù)據(jù)類型產(chǎn)生具體數(shù)據(jù)類型的完備演算法則；●首次為海量并行程序語言BSP語言建立指稱語義和代數(shù)轉(zhuǎn)化方法。主要學(xué)術(shù)成果包括：●首次建立規(guī)范的數(shù)學(xué)模型，并發(fā)現(xiàn)求解規(guī)范方程(X;Q)>S和(P;X)>S的演算法則；●創(chuàng)建基于“上下仿真映照對(duì)”數(shù)據(jù)精化完備理論；●創(chuàng)建程序代數(shù)(He-Hoare代數(shù))，并用它來支持編譯器原型的設(shè)計(jì)和證明；●提出編程統(tǒng)一理論和連接各類程序理論的數(shù)學(xué)法則。軟件演算理論和數(shù)據(jù)精化規(guī)則被譽(yù)為是面向模型軟件開發(fā)的一個(gè)里程碑，是國際標(biāo)準(zhǔn)規(guī)范語言Z的精化理論基礎(chǔ)，是歐洲系統(tǒng)設(shè)計(jì)語言B的軟件開發(fā)方法的理論及基礎(chǔ)。學(xué)科負(fù)責(zé)人還參與了包括歐共體“硬件編譯器”項(xiàng)目在內(nèi)的若干還有一個(gè)技術(shù)難點(diǎn)涉及到軟硬件子系統(tǒng)之間的通訊界面的設(shè)計(jì)，采用傳統(tǒng)方法（同步或異步）使該部件結(jié)構(gòu)規(guī)范化，但會(huì)影響整個(gè)混成系統(tǒng)的性能，并且不利于系統(tǒng)的單芯片實(shí)現(xiàn)方案。為了增加系統(tǒng)的安全性和可移植性，本項(xiàng)目實(shí)施技術(shù)將不固定軟硬件通訊界面的協(xié)議，而根據(jù)用戶對(duì)系統(tǒng)的要求（處理速度、信息量）來設(shè)計(jì)面向應(yīng)用的專用通訊界面。在系統(tǒng)的單芯片實(shí)施方案中，界面描寫最終仍可用硬件來實(shí)現(xiàn)。在設(shè)計(jì)實(shí)時(shí)嵌入式系統(tǒng)中，由于可用的硬件資源限制（性能、功耗、面積），產(chǎn)品的優(yōu)化是一個(gè)重要課題。軟硬件轉(zhuǎn)換器和分解器設(shè)計(jì)中將結(jié)合多類分析優(yōu)化技術(shù)來減少元器件的數(shù)目，增加元器件在硬件子系統(tǒng)中的重用性。將對(duì)應(yīng)的結(jié)構(gòu)重組（Reconfigurable）也是一個(gè)技術(shù)難點(diǎn)。將為軟硬件混合系統(tǒng)的可組合描寫、分析和設(shè)計(jì)提供一個(gè)綜合性的理論框架和設(shè)計(jì)方法，它們具有下屬幾個(gè)特征：（1）它能處理多類函數(shù)和非函數(shù)的需求分析，提出模塊化和優(yōu)化的處理方案。（2）基于形式化技術(shù)，從而保證目標(biāo)產(chǎn)品的可靠性和安全性。（3）能容納多類不同開發(fā)語言，并提供它們之間語義等價(jià)轉(zhuǎn)換的法則。與硬件系統(tǒng)設(shè)計(jì)密切聯(lián)系的軟件方面，規(guī)格說明的形式化及相應(yīng)的開發(fā)方法和驗(yàn)證工具還未設(shè)計(jì)出來。更進(jìn)一步講，許多現(xiàn)有的形式化方法缺乏足夠的應(yīng)用范圍，它們沒有將許多性質(zhì)(如：可靠性、安全性)進(jìn)行組合考慮。軟硬件混合系統(tǒng)關(guān)鍵挑戰(zhàn)是：為硬件、軟件的協(xié)同設(shè)計(jì)尋找一個(gè)統(tǒng)一構(gòu)架，使我們的設(shè)計(jì)能跟上“半導(dǎo)體設(shè)備及相應(yīng)軟件”復(fù)雜性的飛速增加。另外，也要求我們?cè)谶@相同的構(gòu)架內(nèi)，既要解決模擬與數(shù)字設(shè)備，同時(shí)也要解決多時(shí)鐘系統(tǒng)問題。準(zhǔn)備采用IntervalTemporalLogic(即ITL)作為高層規(guī)范的描述工具，與其它邏輯不同，ITL既能用來描述順序系統(tǒng)，又能用來描述并行系統(tǒng)，同時(shí)ITL又強(qiáng)有力地支持工業(yè)界應(yīng)用系統(tǒng)的安全性、實(shí)時(shí)性、可靠性等性質(zhì)。由于模擬方法太花時(shí)間，最終不能絕對(duì)保證硬件設(shè)計(jì)的準(zhǔn)確性。而向?qū)嶋H工業(yè)界應(yīng)用的硬件系統(tǒng)，首先要保證準(zhǔn)確，同時(shí)又要提高開發(fā)速度，所以要研究面向“這些工業(yè)系統(tǒng)”硬件設(shè)計(jì)的軟件開發(fā)方法，“硬件規(guī)范”用ITL來描述，使設(shè)計(jì)的準(zhǔn)確性歸約到上述ITL公式的準(zhǔn)確性。用本學(xué)科研究提供的軟、硬件混合設(shè)計(jì)方法，對(duì)于硬件系統(tǒng)的設(shè)計(jì)而言，只要寫出相應(yīng)的軟件描述即可。學(xué)科負(fù)責(zé)人在英國工作期間已經(jīng)將這類方法使用在SONY公司的VCD穩(wěn)定器和西敏寺銀行的智能卡設(shè)計(jì)上。前者產(chǎn)品成本不到一美元，后者得到了英國工貿(mào)部LEVEL-5產(chǎn)品安全證書（最高可靠性）。無論嚴(yán)格安全軟件理論還是計(jì)算機(jī)軟硬件協(xié)同設(shè)計(jì)，均站在國際前列。三、項(xiàng)目建設(shè)目標(biāo)在嚴(yán)格安全軟件理論與數(shù)據(jù)精化法則方面：具備國際級(jí)影響；形成與歐美相當(dāng)水平的學(xué)派；培養(yǎng)出一個(gè)良好的學(xué)術(shù)梯隊(duì)；并推出計(jì)算機(jī)軟硬件協(xié)同設(shè)計(jì)平臺(tái)，為SOC(SystemOnChip)的設(shè)計(jì)提供先進(jìn)的開發(fā)工具。這將是典型的具有原創(chuàng)性和自主知識(shí)產(chǎn)權(quán)的產(chǎn)、學(xué)、研密切結(jié)合的標(biāo)志性成果。我國SOC能力十分薄弱，在汽車、航天、家電、醫(yī)療行業(yè)和金融界等，這樣的平臺(tái)有著極為廣泛的應(yīng)用前景。現(xiàn)在，我國研究人員往往去西方發(fā)達(dá)國家學(xué)習(xí)、訪問。建議重點(diǎn)學(xué)科若被批準(zhǔn)，相信國外的研究人員將到這里來學(xué)習(xí)、訪問。四、項(xiàng)目建設(shè)所需經(jīng)費(fèi)本項(xiàng)目建設(shè)總投入經(jīng)費(fèi)900萬元，其中中央專項(xiàng)資金100萬元（即國家計(jì)委100萬元），上海市政府配套100萬元，學(xué)校自籌資金（學(xué)校教育產(chǎn)業(yè)及事業(yè)收費(fèi)收入等）700萬元。具體資金投向?yàn)椋涸O(shè)備與環(huán)境730萬元；國際學(xué)術(shù)活動(dòng)70萬元；學(xué)科建設(shè)資料100萬元。本項(xiàng)目擬購的代表性儀器設(shè)備有：SUN服務(wù)器、主要用于協(xié)同計(jì)算的IBM主機(jī)、用于科學(xué)計(jì)算的IBM小型機(jī)等。五、項(xiàng)目建設(shè)已有條件、優(yōu)勢和特點(diǎn)學(xué)科所在的軟件學(xué)院是國家35所軟件學(xué)院之一，學(xué)校、復(fù)星高科技集團(tuán)、國家外國專家局和海外銀行在政策和財(cái)力方面給予了各種支持。國家軟件人才國際培訓(xùn)（上海）基地，是江、浙、滬唯一的這類基地。原有“計(jì)算機(jī)軟件與理論”、“計(jì)算機(jī)應(yīng)用”和“系統(tǒng)分析與集成”等點(diǎn)是學(xué)科發(fā)展的依托。2000年6月27日，國務(wù)