【基金標書】2010CB328000-現(xiàn)代設計大型應用軟件的可信性研究

《【基金標書】2010CB328000-現(xiàn)代設計大型應用軟件的可信性研究》由會員分享，可在線閱讀，更多相關(guān)《【基金標書】2010CB328000-現(xiàn)代設計大型應用軟件的可信性研究（15頁珍藏版）》請在裝配圖網(wǎng)上搜索。

項目名稱： 現(xiàn)代設計大型應用軟件的可信性研究首席科學家： 孫家廣 清華大學起止年限： 2010年 1月-2014 年 8月依托部門： 教育部一、研究內(nèi)容在現(xiàn)代制造業(yè)，隨著產(chǎn)品設計規(guī)模和設計難度的增加，設計系統(tǒng)和產(chǎn)品設計過程的復雜性越來越高，個性化設計需求越來越強烈，設計活動越來越突出地體現(xiàn)了知識密集性和通訊密集性的特點。本項目將圍繞三個科學問題，對產(chǎn)品設計過程和設計模型的可用性、安全性、可靠性和可驗證性等可信性內(nèi)容進行深入研究。主要研究內(nèi)容有以下幾個方面：? 產(chǎn)品模型數(shù)據(jù)表示和計算誤差可控性以及模型表示的一致性，以提高設計過程中數(shù)據(jù)表示可信性；? 設計系統(tǒng)程序代碼與規(guī)約說明的一致性驗證，以提高設計系統(tǒng)程序代碼的正確性；? 產(chǎn)品設計流程的可信保障機制，以解決產(chǎn)品數(shù)據(jù)模型在全生命周期的一致性；? 基于 GPU 集群的數(shù)字模型仿真優(yōu)化計算，以保證產(chǎn)品交互設計的一致性和高效性；? 構(gòu)建產(chǎn)品設計與仿真優(yōu)化交互設計平臺，以增強產(chǎn)品功能和性能仿真優(yōu)化設計的實用性和可靠性。 2.1 產(chǎn)品數(shù)據(jù)模型表示的一致性及其誤差控制理論2.1.1 復雜產(chǎn)品數(shù)據(jù)模型的高精度表示及其誤差控制研究表示復雜產(chǎn)品的新型數(shù)據(jù)結(jié)構(gòu)，研究產(chǎn)品數(shù)字模型中幾何操作的誤差精度控制方法，研究設計過程誤差精度統(tǒng)一表示（研究產(chǎn)品設計誤差以及各設計環(huán)節(jié)的誤差關(guān)聯(lián)約束）和產(chǎn)品數(shù)據(jù)表示誤差和設計過程誤差的約束、傳播和擴散機制，研究產(chǎn)品設計輕量化表示中的精度保持方法。1、幾何運算中的誤差精度控制本項目將幾何運算分解成為底層的單元幾何運算和高層次的特征幾何運算。研究從單元幾何運算到高層次特征幾何運算的誤差傳播機制，設法統(tǒng)一同一階段的不同單元幾何運算的誤差精度控制方法，設法統(tǒng)一不同階段的單元幾何運算的誤差精度控制方法。研究在產(chǎn)品設計過程中統(tǒng)一的幾何運算誤差精度控制理論和方法。2、設計過程誤差精度統(tǒng)一表示本項目將分析在產(chǎn)品設計周期中從產(chǎn)品概念設計、幾何設計到結(jié)構(gòu)設計及其迭代分析過程中各種相關(guān)數(shù)據(jù)之間的對應關(guān)系，對精度的要求，以及在實際操作過程中所能達到的誤差精度。同時將分析和總結(jié)在產(chǎn)品設計周期中所涉及到的誤差種類。在此基礎上，將形成產(chǎn)品設計過程的誤差精度統(tǒng)一表示理論和方法，研究誤差動態(tài)控制理論和技術(shù)，以適應在產(chǎn)品設計周期中各個階段以及迭代過程的誤差不斷積累及動態(tài)發(fā)生變化的情況。由此進一步規(guī)范產(chǎn)品設計的實現(xiàn)手段，形成與其相適應的理論和方法。本項目將研究產(chǎn)品設計數(shù)據(jù)的輕量化表示方法及其精度保持的策略。還將研究有損精度和無損精度的多種數(shù)據(jù)壓縮理論和策略，進一步控制幾何和非幾何數(shù)據(jù)的規(guī)模。將進一步研究各多層次模型之間的精度度量理論和策略。2.1.2 面向產(chǎn)品設計全生命周期的數(shù)據(jù)模型和設計過程的一致性度量本項目將研究復雜產(chǎn)品設計手段可達性，研究產(chǎn)品數(shù)據(jù)模型的結(jié)構(gòu)特征的語義表示方法，研究產(chǎn)品迭代設計過程中數(shù)據(jù)模型修改中的結(jié)構(gòu)特征約束方法，研究產(chǎn)品結(jié)構(gòu)特征模型的可重用度量方法，研究產(chǎn)品全生命周期的設計迭代交互過程中的數(shù)據(jù)模型統(tǒng)一表示（研究異構(gòu)系統(tǒng)或者設計流程各設計環(huán)節(jié)之間的數(shù)字模型數(shù)據(jù)轉(zhuǎn)換機制）和研究產(chǎn)品全設計流程的數(shù)據(jù)表示完整性。1、產(chǎn)品設計過程的數(shù)據(jù)模型表示一致性產(chǎn)品設計過程中，從 CAD 的部件設計到 CAE 有限元優(yōu)化設計，再回到CAD 數(shù)據(jù)模型設計，設計過程迭代反復修改，但是整個設計過程需要考慮產(chǎn)品設計手段是否能夠滿足設計全過程的要求，也就是需要考慮設計全過程的設計手段的可達性，同時也需要考慮產(chǎn)品模型的覆蓋域和產(chǎn)品表示的完備性，使得產(chǎn)品設計過程方便快速，產(chǎn)品數(shù)據(jù)模型表示一致和完備。同時將考慮產(chǎn)品模型中的各種特征的提取方法和特征與產(chǎn)品模型之間的約束關(guān)系及其度量方法，在產(chǎn)品迭代修改過程中，產(chǎn)品模型中的結(jié)構(gòu)特征必須與數(shù)據(jù)模型保持相對應的約束關(guān)系，產(chǎn)品特征在設計修改過程中具有特征的一貫性和連續(xù)性，同時還研究異構(gòu)系統(tǒng)中模型數(shù)據(jù)之間的數(shù)據(jù)轉(zhuǎn)換機制，考慮模型特征的連貫性，產(chǎn)品特征的可重用性，以保證模型數(shù)據(jù)的一致性，為此將研究可重用特征的設計邏輯一致性和可重用的度量方法。2、基于設計時序關(guān)系和邏輯關(guān)系的設計迭代求精從時序性關(guān)系角度，產(chǎn)品設計流程與規(guī)范可以被描述為一系列時間節(jié)點所構(gòu)成的子任務行為及其迭代的集合。 “邏輯關(guān)系” 是設計流程與規(guī)范間的一種抽象，這種抽象的關(guān)系主要體現(xiàn)在設計主體對設計目標及設計系統(tǒng)認知的深度及抽象性上。邏輯關(guān)系在更深的層次上揭示了產(chǎn)品特征設計和數(shù)據(jù)流的相互作用和結(jié)構(gòu)關(guān)系的相互制約，包括設計目標的表征、設計特征提取及語義化描述；設計過程中語義演化及物理造型屬性的迭代過程。建立符合人的預期的產(chǎn)品設計迭代求精機制，為基于領(lǐng)域知識的復雜產(chǎn)品設計迭代模型和領(lǐng)域任務的一致性和可度量性奠定基礎。2.2 支持產(chǎn)品全生命周期的交互設計系統(tǒng)的可驗證理論2.2.1 產(chǎn)品設計系統(tǒng)的程序代碼可驗證理論研究產(chǎn)品數(shù)據(jù)模型中幾何算法和幾何操作的程序自動驗證方法，研究產(chǎn)品設計系統(tǒng)構(gòu)件及其組裝的程序健壯性和可靠性。1、程序代碼與規(guī)約說明的一致性驗證現(xiàn)代設計軟件中包含了大量的算法及其實現(xiàn)代碼。如何對算法進行形式化規(guī)約說明，如何保證代碼的最終實現(xiàn)與算法的規(guī)約說明一致，是本項目要研究的重要內(nèi)容，為此，將研究基于類型論的命令式程序表示方法和算法的模塊化規(guī)范描述和證明等問題。2、基于模型檢測的程序驗證技術(shù)在大型設計軟件的編碼過程中，除了由于代碼實現(xiàn)與規(guī)約說明不一致而造成的邏輯錯誤之外，還存在大量由于編碼人員的熟練程度和編碼水平而產(chǎn)生的代碼缺陷。本項目擬研究將模型檢測應用于現(xiàn)代設計軟件核心代碼的自動驗證，通過謂詞抽象等方法縮減狀態(tài)空間和映射無窮域，避免狀態(tài)空間爆炸。另一方面，考慮到現(xiàn)代設計軟件程序中涉及大量有關(guān)數(shù)組、向量、矩陣等的數(shù)值操作，我們也將研究針對這些特定數(shù)據(jù)結(jié)構(gòu)的程序驗證方法學。2.2.2.按需組裝的產(chǎn)品全設計流程的一致性驗證產(chǎn)品設計的可信性包括產(chǎn)品全生命周期的可維護性和可靠性，產(chǎn)品全生命周期從需求分析、概念設計、概要設計和詳細設計，再到產(chǎn)品的具體設計過程的幾何設計、結(jié)構(gòu)設計到 CAE 仿真模擬，再到產(chǎn)品制造銷售、產(chǎn)品使用維護乃至產(chǎn)品回收處理等全過程，因此產(chǎn)品可信性設計不僅需要考慮產(chǎn)品具體的產(chǎn)品設計流程及其迭代設計，而且還需要考慮產(chǎn)品全生命周期的全過程質(zhì)量控制和管理。本項目的主要研究內(nèi)容包括產(chǎn)品設計全流程質(zhì)量控制機制、產(chǎn)品數(shù)據(jù)模型表示全流程一致性等內(nèi)容，基于產(chǎn)品全流程的產(chǎn)品設計系統(tǒng)主要包括軟件系統(tǒng)的設計、構(gòu)件集成再到交互操作和產(chǎn)品統(tǒng)一數(shù)據(jù)表示模型、復雜產(chǎn)品交互設計系統(tǒng)的可用性和易用性度量等。同時將研究產(chǎn)品迭代設計過程中的需求一致性問題，解決設計系統(tǒng)過程中的功能需求的迷路問題，解決產(chǎn)品設計和驗證的信息孤島問題，本項目將研究產(chǎn)品設計中的數(shù)據(jù)安全問題等。研究產(chǎn)品設計數(shù)據(jù)自保護安全信任模型,數(shù)據(jù)存儲、處理、傳輸?shù)臋C密性和完整性等保護，研究產(chǎn)品設計數(shù)據(jù)內(nèi)核級自保護技術(shù)，研究設計數(shù)據(jù)安全訪問許可策略及多約束力的使用許可協(xié)議。2.3 產(chǎn)品功能和性能高效仿真優(yōu)化理論和方法2.3.1 產(chǎn)品功能設計的仿真計算方法研究基于產(chǎn)品 CAD 模型的仿真方法，研究產(chǎn)品幾何設計與功能設計迭代優(yōu)化仿真方法。研究基于線性插值單元理論的高精度仿真計算方法，建立自主開發(fā)而且具有較強工程應用能力的仿真軟件。研究基于產(chǎn)品 CAD 模型的仿真計算理論與方法，研究基于 GPU 的計算方法，利用圖形卡的并行性能和高密集的運算性能，來實現(xiàn)一般意義上的計算，針對大規(guī)模數(shù)值計算部分進行 GPU 并行化。2.3.2 復雜產(chǎn)品結(jié)構(gòu)組合的高效仿真計算與優(yōu)化研究多領(lǐng)域多學科產(chǎn)品優(yōu)化計算及其并行仿真可視化方法，研究基于 GPU集群的復雜產(chǎn)品系統(tǒng)性能優(yōu)化設計方法。通過建立高效的優(yōu)化設計模塊，建立自主研發(fā)的復雜產(chǎn)品設計優(yōu)化平臺。建立基于 GPU 構(gòu)架的并行優(yōu)化程序，解決復雜性中等的實際工程問題，研究基于 GPU 構(gòu)架的并行智能布點技術(shù)，研究混合近似模型技術(shù)，通過不同方法近似模型的組合，加強近似模型的魯棒性和精度。并行仿真模擬計算得到的大規(guī)模數(shù)據(jù)，通過有效的可視化顯示，可以更有效地對產(chǎn)品設計功能性能進行分析驗證，本項目將研究基于特征分析的高質(zhì)量大規(guī)模數(shù)據(jù)可視化算法，研究面向多核、分布式集群、GPU、GPU 集群以及網(wǎng)格環(huán)境的大規(guī)模仿真數(shù)據(jù)并行可視化算法。二、預期目標3.1 總體目標本項目旨在面向重大制造裝備和復雜產(chǎn)品設計等重要應用領(lǐng)域展開CAD/CAE 大型應用軟件的可信性研究，建立重大制造裝備和復雜產(chǎn)品模型的統(tǒng)一數(shù)據(jù)表示，保證幾何設計、結(jié)構(gòu)設計、模型分析和仿真驗證等各環(huán)節(jié)迭代求精和分析在產(chǎn)品設計生命周期中的一致性，提供系統(tǒng)構(gòu)件之間的可驗證機理，建立數(shù)據(jù)和模型的多級安全動態(tài)保護理論和策略，給出應用軟件的可信度分析方法，為提高我國汽車、重大制造裝備等復雜產(chǎn)品的國際競爭力，提供其自主創(chuàng)新的理論和技術(shù)支撐。本項目總體研究水平力求進入國際先進行列，力爭在以下三個方面取得創(chuàng)新突破：產(chǎn)品數(shù)字模型表示的誤差控制和一致性理論與技術(shù)；設計系統(tǒng)程序代碼的正確性驗證理論與方法；產(chǎn)品功能和性能的仿真優(yōu)化設計理論與技術(shù)。以期在國產(chǎn)品牌汽車和重大裝備制造的創(chuàng)新設計與仿真優(yōu)化中得到成功應用。項目擬完成 15-20 項有自主知識產(chǎn)權(quán)的核心算法或軟件技術(shù)（包括技術(shù)專利和版權(quán)登記） 。本項目擬在國內(nèi)外核心刊物和國際會議上發(fā)表論文 30-50 篇/ 年，其中國際刊物與國際會議論文集的論文發(fā)表 12-18 篇/ 年；學術(shù)著作 3 部，技術(shù)報告平均 10 篇/年；博士論文平均 12 篇/年。力爭本項目 80％以上的研究成果、技術(shù)標準、規(guī)范和專利等被轉(zhuǎn)化到國家 863 計劃或科技支撐計劃，為我國現(xiàn)代設計大型應用軟件的研究開發(fā)與應用提供高效可靠的技術(shù)支撐，在汽車和 IC 裝備復雜機械部件的設計與制造領(lǐng)域?qū)嶋H應用，產(chǎn)生明顯的經(jīng)濟和社會效益。3.2 五年預期目標上述目標將分階段分步實施。根據(jù)目前的工作基礎、未來五年的研究目標大致可分為以下三部分，具體敘述如下。3.2.1 產(chǎn)品設計數(shù)據(jù)表示模型和設計系統(tǒng)的可信性度量理論將研究以下關(guān)鍵內(nèi)容并取得重要進展：1、 復雜產(chǎn)品數(shù)據(jù)模型的高精度數(shù)據(jù)表示及其誤差控制；2、 面向產(chǎn)品設計全生命周期的產(chǎn)品數(shù)據(jù)和設計過程的一致性度量；3、 產(chǎn)品設計系統(tǒng)的程序代碼可驗證理論；4、 按需組裝的產(chǎn)品全設計流程的一致性驗證。3.2.2 產(chǎn)品數(shù)據(jù)模型的一致性驗證及產(chǎn)品功能與性能的高效仿真模擬將研究以下關(guān)鍵內(nèi)容并取得重要進展：1、 產(chǎn)品數(shù)據(jù)模型功能設計的仿真優(yōu)化；2、 復雜產(chǎn)品結(jié)構(gòu)組合的高效仿真計算。同時，將研究開發(fā)一個用戶設計復雜產(chǎn)品及其功能與性能仿真模擬的大型設計軟件平臺，集成上述各關(guān)鍵科學問題的研究成果，確保設計數(shù)據(jù)處理的靈活性和可擴展性；克服數(shù)據(jù)本身的異構(gòu)性和系統(tǒng)的異構(gòu)性引起的不協(xié)調(diào)性，即時審計入侵等不安全因素，使該核心平臺安全、可靠、實用。3.2.3 集成應用檢驗結(jié)合汽車和 IC 裝備等復雜機械部件在現(xiàn)代設計方面的實際需求，研究開發(fā)現(xiàn)代設計大型應用軟件系統(tǒng)，并在實際應用中取得經(jīng)濟和社會效益。這部分工作實際上是對前兩部分研究成果的集成和實際應用檢驗。三、研究方案4.1 總體思路項目將圍繞總體研究目標和主要研究內(nèi)容，結(jié)合以汽車設計為應用背景組織實施研究技術(shù)方案，項目的總體研究思路和總體設計方案框架如圖 1 所示。圖 1. 現(xiàn)代設計大型應用軟件系統(tǒng)可信核心平臺框架本項目在技術(shù)途徑方面擬考慮以下幾點：（1） 可信性基礎與系統(tǒng)仿真和驗證平臺同步研究把握對現(xiàn)代設計大型應用軟件有重要影響的可信性理論集中力量優(yōu)先突破，并持之以恒，毫不動搖，本項目列出的三個關(guān)鍵科學問題均屬此列。在進行共性基礎研究的同時，從頂層著手現(xiàn)代設計大型應用軟件平臺與系統(tǒng)的設計與研發(fā)，因為這個平臺是單元設計行為和設計過程可信性研究的集成試驗床，不盡早拿出這個平臺，各關(guān)鍵技術(shù)的測試與試運行就難以進行。相反，可信性理論與驗證和仿真系統(tǒng)平臺同步研究，雙方還有相互促進，相互補充的作用。（2） 理論研究與實踐檢驗相結(jié)合本項目的可信性理論具有鮮明的實踐性，無論是產(chǎn)品數(shù)據(jù)模型的高精度表示模型，還是產(chǎn)品設計過程的一致性表示，既具有深奧的理論又貼近實踐。理論行不行，好不好，完全要用實踐來檢驗，而實踐中發(fā)生的問題又推動理論研究更加深入，更加全面。因此，本項目具有理論與實踐緊密結(jié)合，理論指導實踐，實踐提出問題與需求，促進理論的深入與發(fā)展的特點。（3） 既注意獨立開發(fā)，有自主知識產(chǎn)權(quán)，又注意學習國外先進內(nèi)容，洋為中用，走引進、吸收、消化、創(chuàng)新之路，切實貫徹有所為、有所不為，但一定要有所作為。（4） 在注意建立自己的技術(shù)標準和規(guī)范的同時，更要認真學習，貫徹執(zhí)行國際相關(guān)標準，積極參加國際相關(guān)的技術(shù)規(guī)范聯(lián)盟，如：OMG、 XML、RIG、STEP 等。4.2 技術(shù)路線整個項目的技術(shù)路線圍繞著本項目的三個科學問題展開的，具體落實到本項目的五個課題分解進行:1. 針對復雜產(chǎn)品數(shù)據(jù)模型精度可控性理論和方法的研究，其中的技術(shù)路線為： ? 分析并建立多精度層次的數(shù)據(jù)模型及其映射關(guān)系，形成產(chǎn)品設計周期中誤差類型及其傳播和擴散機制。? 針對汽車和重大制造裝備等產(chǎn)品的設計全生命周期，分析產(chǎn)品各種數(shù)據(jù)表示及其關(guān)聯(lián)關(guān)系，研究各種數(shù)據(jù)的異構(gòu)和同構(gòu)屬性，形成設計全生命周期的產(chǎn)品數(shù)據(jù)誤差統(tǒng)一表示理論和方法。? 基于國內(nèi)外行業(yè)和企業(yè)標準，采用優(yōu)化方法，建立統(tǒng)一產(chǎn)品數(shù)據(jù)模型的輕量化表示理論和方法，降低數(shù)據(jù)的冗余程度，提高模型數(shù)據(jù)的應用效率。 首先將研究在單元幾何運算中的誤差精度控制理論和方法，研究在曲線曲面求交、延伸、擬合等運算中的誤差精度控制機理，分析其誤差產(chǎn)生機理和誤差可控類型。在此基礎上，研究拉伸、抽殼和拔模等高層次的幾何特征操作。本項目將利用區(qū)間理論及其運算方法記錄并分析在產(chǎn)品設計周期中誤差的傳播和擴散機制，從而進一步挖掘誤差調(diào)控機理，進而提高設計和分析精度，分析和總結(jié)在產(chǎn)品設計周期中所涉及到的誤差種類。明確各類誤差的含義，確定它們之間的關(guān)聯(lián)，形成相應的誤差精度統(tǒng)一表示理論和方法。從而，采用迭代的策略，重新將其應用于產(chǎn)品設計周期中概念設計、幾何設計、結(jié)構(gòu)設計和優(yōu)化設計以及迭代分析過程中，跟蹤、記錄和分析在產(chǎn)品設計周期中誤差的傳播和擴散機制，從而進一步修正誤差精度統(tǒng)一表示理論和方法。2. 針對產(chǎn)品設計全流程一致性理論和方法的研究，其中的技術(shù)路線為： ? 利用數(shù)據(jù)模型在設計制造全流程中的表示差異性，確保模型格式轉(zhuǎn)換的精度保持，使得迭代設計可反饋可驗證，保證模型表示的完備性，提高設計制造效率。? 采用數(shù)據(jù)模型特征的提取方法，通過探索異構(gòu)環(huán)境下各種特征的語義表示方法，確保特征在整個設計流程的一致性表述。 ? 通過數(shù)據(jù)模型的語義特征，在模型編輯功能中實現(xiàn)特征可復用。產(chǎn)品設計與制造涉及產(chǎn)品設計、功能驗證和制造各個環(huán)節(jié)，為此需要研究建立產(chǎn)品設計全生命周期的產(chǎn)品數(shù)據(jù)統(tǒng)一表示理論和方法，統(tǒng)一不同階段不同環(huán)節(jié)的產(chǎn)品數(shù)據(jù)，可以減少因為數(shù)據(jù)不統(tǒng)一所造成的產(chǎn)品表達不一致性，從而為整個設計過程具有高效性、可維護性、可拓展性提供統(tǒng)一數(shù)據(jù)表示。如果簡單地將各種數(shù)據(jù)疊加在一起，一方面會造成數(shù)據(jù)的大量冗余并容易造成數(shù)據(jù)的不一致性，另一方面會造成數(shù)據(jù)非常龐大，從而實際上會增加產(chǎn)品設計的復雜程度并降低產(chǎn)品設計的規(guī)模。為此，將針對汽車和重大制造裝備等產(chǎn)品的設計全生命周期，分析產(chǎn)品幾何設計、結(jié)構(gòu)設計、優(yōu)化設計以及迭代過程等所需要的各種數(shù)據(jù)表示，以及這些數(shù)據(jù)之間的關(guān)聯(lián)關(guān)系，研究各種數(shù)據(jù)的異構(gòu)和同構(gòu)屬性，形成設計全生命周期的產(chǎn)品數(shù)據(jù)統(tǒng)一表示理論和方法。同時還研究統(tǒng)一產(chǎn)品數(shù)據(jù)模型的數(shù)據(jù)輕量化表示理論和方法，盡可能降低數(shù)據(jù)的冗余程度，提高數(shù)據(jù)的應用效率。在統(tǒng)一產(chǎn)品數(shù)據(jù)的數(shù)據(jù)輕量化過程中，將建立有效的屬性繼承和傳播機制，從而盡可能讓數(shù)據(jù)在產(chǎn)品設計全生命周期中不丟失、能演化、能自動關(guān)聯(lián)。因此，我們還將研究數(shù)據(jù)的交換和轉(zhuǎn)化理論和方法，從而進一步減少產(chǎn)品核心數(shù)據(jù)模型的數(shù)據(jù)量，便于不同的設計過程或階段獲取與其相適應的數(shù)據(jù)。3. 針對產(chǎn)品設計軟件系統(tǒng)的程序代碼可驗證性理論的研究，其中的技術(shù)路線為：? 分析產(chǎn)品設計軟件算法的領(lǐng)域特征，兼顧可驗證的需求，設計算法規(guī)范說明語言。? 基于高階邏輯和定理證明系統(tǒng)，構(gòu)建算法規(guī)約說明推理系統(tǒng)，提供算法層面上的正確性驗證框架。? 利用模型檢測技術(shù)，采用謂詞抽象和可滿足性模理論，實現(xiàn)代碼層面的程序驗證框架。算法關(guān)注于解決問題的方法和邏輯。為算法提供一種形式化描述語言是對其正確性進行檢驗的前提基礎。為此，需要根據(jù)現(xiàn)代設計軟件中核心算法的特點，研究適合于此類應用的形式化描述語言。我們將在分析現(xiàn)有算法說明語言的基礎之上，基于一階邏輯和集合論，針對現(xiàn)代設計軟件常用的一些復雜數(shù)據(jù)結(jié)構(gòu)及其操作，設計算法規(guī)范說明語言。命令式程序的表示關(guān)鍵是對內(nèi)存模型的描述。我們將采用最弱前置條件和函數(shù)式語言解釋等方法，設計一個新的更低層次的內(nèi)存模型。該內(nèi)存模型在邏輯層次上考慮，而命令式語言的各種成分可以在該模型下進行解釋。應用模型檢測進行驗證的最大困難來自于狀態(tài)空間爆炸問題。我們將研究如何將謂詞抽象技術(shù)與反例導向的抽象精化技術(shù)結(jié)合。為得到精確的程序抽象模型,重點研究謂詞發(fā)現(xiàn)和冗余謂詞消去技術(shù)。傳統(tǒng)的模型檢測技術(shù)只能在布爾邏輯框架下應用。為了提高模型檢測技術(shù)在程序驗證中的能力，需要研究可滿足性模理論（Satisifiability Modulo Theory, SMT） 。我們將遞進式的研究帶入多個公理域的邏輯公式可滿足性判定理論，重點研究線性不等式、數(shù)組、向量等理論域的判定算法。4. 針對產(chǎn)品設計流程可信保障機理的研究，其中的技術(shù)路線為： ? 采用基于 WBS 的流程建模方法，并內(nèi)嵌元數(shù)據(jù)規(guī)則管理器，實現(xiàn)流程約束、規(guī)則約束和資源約束。? 采用基于刻面的需求工程（AOSD）來消除需求衰減和需求歧義。? 采用著色 Petri 網(wǎng)和模型檢測等形式化工具來保障設計流程中的各種一致性驗證。? 采用面向虛擬組織的復雜訪問控制機制來支持跨自治域的協(xié)同數(shù)據(jù)訪問控制。針對設計流程建模及資源約束機制的研究，將在模型驅(qū)動理論的基礎上，重點解決以 WBS為核心的設計過程統(tǒng)一視圖問題及設計資源元數(shù)據(jù)的統(tǒng)一標準問題。在 WBS模型的基礎上，引入資源元數(shù)據(jù)模型，支持動態(tài)資源映射和評估分析；引入擴展流程模型，支持動態(tài)的設計過程建模及監(jiān)控；引入時序約束，保證設計過程的可信性和執(zhí)行的準確性。針對產(chǎn)品設計及流程的安全保障機制，將根據(jù)設計過程中的安全需求，在通用安全基礎設施的基礎上，重點解決設計過程的實體識別、基于信任的訪問控制機制、數(shù)據(jù)保護等問題。此外，針對現(xiàn)代協(xié)同設計的特點，還將解決跨自治域的復雜訪問控制、協(xié)同環(huán)境下的數(shù)據(jù)分發(fā)及協(xié)同設計過程中的隱私保護等問題，并最終為總課題的應用提供安全保障。5. 針對產(chǎn)品功能和性能高效仿真優(yōu)化理論與方法的研究，其中的技術(shù)路線為： ? 采用光滑單元理論，提高線性插值單元的計算精度，實現(xiàn)低階單元網(wǎng)格的自適應分割，提升數(shù)據(jù)模型的網(wǎng)格生成質(zhì)量和生成速度。? 以 Cg 和 CUDA 為手段，建立基于 GPU 集群的高效求解體系，實現(xiàn)廉價的快速仿真計算。? 探索基于 GPU、多核 CPU 以及分布式集群間任務高效劃分和實時調(diào)度方法，大幅度提高交互可視化呈現(xiàn)速度。? 對優(yōu)化領(lǐng)域中的多目標、多目標、多學科、多參數(shù)、不確定性這幾方面的技術(shù)瓶頸進行研究，結(jié)合 GPU 技術(shù)，研發(fā)具有能處理實際工程問題的優(yōu)化軟件平臺。? 將仿真分析、優(yōu)化算法進行整合，構(gòu)建一個高可信、全構(gòu)件的設計仿真優(yōu)化集成應用平臺。本項目建立的復雜產(chǎn)品設計平臺是傳統(tǒng) CAE 軟件應用的提升，簡單封閉的前處理體系，基于 GPU 的高效求解體系以及自主研發(fā)的近似模型優(yōu)化體系是該系統(tǒng)性能和實用性的保證。通過提出新型單元理論，并采用基于 GPU 的求解技術(shù)，以解決復雜產(chǎn)品功能和性能仿真優(yōu)化中的效率和可靠性兩大瓶頸問題，在此基礎上，形成一個具有重大創(chuàng)新和實用價值的仿真模擬和優(yōu)化設計平臺，并在我國的汽車設計制造中得到成功應用。四、年度計劃年度 研究內(nèi)容 預期目標第一年1. 精確浮點數(shù)運算算法及新的實數(shù)表示方法研究。2. 調(diào)研并分析產(chǎn)品數(shù)據(jù)模型的表示格式類型、標準及其特征表示。3. 研究 NURBS與離散網(wǎng)格之間的模型格式轉(zhuǎn)換，保持產(chǎn)品設計轉(zhuǎn)移過程的誤差要求。4. 算法規(guī)約說明語言、謂詞抽象計算方法研究5. 現(xiàn)代設計流程及設計資源配置情況調(diào)研6. 支持可信設計過程的動態(tài) WBS的建模方法和理論、基于元數(shù)據(jù)的編碼及規(guī)則控制方法研究。7. 支持可信設計過程的安全保障體系研究。8. 研究基于線性插值單元理論的高精度仿真計算方法。9. 研究基于新型單元和 GPU 的顯式有限元程序開發(fā)、實時計算1. 給出公式化得到浮點數(shù)特性的方法，提出全新的基于 Sierpinski三角形坐標表示實數(shù)的方法。2. 提交至少一種數(shù)據(jù)模型格式轉(zhuǎn)換模塊并可演示。3. 明確算法規(guī)約說明語言的語法和語義；提出適用于此類程序的謂詞計算方法。4. 形成針對汽車、軌道交通等特定行業(yè)設計流程及設計資源配置的研究報告。5. 提出支持可信設計過程的動態(tài) WBS的建模理論、基于元數(shù)據(jù)的編碼及規(guī)則控制理論。6. 提出可信設計過程的安全保障體系理論。7. 建立精度級別達到四邊形和六面體單元的新型單元模型，開發(fā)出基于新型三角形、四面體單元和 GPU的顯式有限元程序。8. 開發(fā)出基于 GPU 的薄板成形及結(jié)構(gòu)碰撞過程的計算機仿真軟件系統(tǒng)第二年1. 新實數(shù)表示下的各種復雜的精確實數(shù)運算算法、高精度的單元幾何運算以及誤差控制研究。2. 研究常見的產(chǎn)品數(shù)據(jù)模型的表示格式類型及標準、特征抽取及表示。3. 算法說明語言的推理證明、向量理論域的可判定理論研究。4. 自動定理證明工具擴展5. 研究資源統(tǒng)一標準的管理方法6. 構(gòu)建資源標準建模體系、資源元數(shù)據(jù)建模工具集。1. 新算法在曲線曲面求交、延伸、擬合等運算中的取得高精度結(jié)果以及可控的誤差。2. 研制的特征提取和復用的原型系統(tǒng)可演示。3. 提出算法規(guī)約說明的推理證明系統(tǒng)，并在產(chǎn)品設計軟件的算法程序中進行實例分析。4. 在 FOPIC基礎之上，對向量數(shù)據(jù)類型進行擴展，支持對向量數(shù)據(jù)類型年度 研究內(nèi)容 預期目標7. 研究資源統(tǒng)一標識和多視圖理論8. 研究面向協(xié)同設計的訪問控制機制、面向協(xié)同設計的數(shù)據(jù)分發(fā)及隱私保護機制。9. 研究基于產(chǎn)品 CAD模型的仿真計算理論與方法、基于實時計算的并行優(yōu)化設計技術(shù)、混合近似模型技術(shù)。的自動定理證明。5. 構(gòu)建資源元數(shù)據(jù)建模工具集。6. 實現(xiàn) CAD 和 CAE 系統(tǒng)的無縫連接和計算分析的自動化，開發(fā)基于GPU 構(gòu)架的并行優(yōu)化程序。第三年1. 研究高精度高層次的特征幾何運算以及誤差控制、區(qū)間運算理論與算法。2. 研究 CAD格式 IGES和 STEP等標準格式，研究離散模型表示格式3. 研究模型的特征表示復用方法及其度量方法4. 研究基于類型論的命令式程序表示方法5. 數(shù)組理論域的可判定理論研究6. 自動定理證明工具擴展7. 研究基于 WBS的流程構(gòu)建方法及工具8. 研發(fā)基于透明加解密的設計文檔保護系統(tǒng)。9. 研究基于 GPU構(gòu)架的并行智能布點技術(shù)，研發(fā)復雜產(chǎn)品優(yōu)化設計平臺。1. 對拉伸、抽殼和拔模等高層次的幾何特征操作中取得高精度結(jié)果以及可控的誤差，找到統(tǒng)一的誤差表示模型。2. 完成至少 3種常用數(shù)據(jù)模型格式的轉(zhuǎn)換工具并可演示。3. 基于 COQ工具，提出對命令式程序的一般性表示方法。4. 在 FOPIC基礎之上，對數(shù)組數(shù)據(jù)類型進行擴展，支持對數(shù)組數(shù)據(jù)類型的自動定理證明。5. 提出基于 WBS和工作流的動態(tài) WBS理論，構(gòu)建基于 WBS的流程建模工具集6. 開發(fā)基于透明加解密的設計文檔保護原型系統(tǒng)。7. 針對不同優(yōu)化對象，構(gòu)建復雜產(chǎn)品優(yōu)化設計平臺。年度 研究內(nèi)容 預期目標第四年1. 研究產(chǎn)品設計周期中誤差類型及其傳播和擴散機制，產(chǎn)品各種數(shù)據(jù)表示及其關(guān)聯(lián)關(guān)系，各種數(shù)據(jù)的異構(gòu)和同構(gòu)屬性。2. 研究離散模型的格式與 CAD常見格式之間的轉(zhuǎn)換方法，多分辨率模型表示格式和輕量化表示格式，特征表示的語義定義方法和特征縫合方法，并研制相應的工具集。3. 研究謂詞發(fā)現(xiàn)方法、冗余謂詞消去方法，開發(fā)程序驗證工具。4. 研究基于動態(tài) WBS的設計過程可視化交互模式，研發(fā)動態(tài) WBS可視化表現(xiàn)工具5. 研發(fā)基于隱私保護的設計文件分發(fā)系統(tǒng)6. 研究基于特征分析的高質(zhì)量大規(guī)模數(shù)據(jù)可視化算法。1. 分析歸納出所有誤差類型以及其傳播擴散機理，形成設計全生命周期的產(chǎn)品數(shù)據(jù)誤差統(tǒng)一表示理論和方法。2. 將特征復用系統(tǒng)在汽車設計等應用中進行應用驗證。3. 開發(fā)面向幾何算法程序的驗證工具。4. 完成動態(tài) WBS交互工具。5. 完成基于隱私保護的設計文件分發(fā)系統(tǒng)。6. 實現(xiàn)基于特征分析的高質(zhì)量大規(guī)模數(shù)據(jù)可視化算法，以及面向多核、分布式集群、GPU、GPU 集群以及網(wǎng)格環(huán)境的大規(guī)模仿真數(shù)據(jù)并行可視化算法。第五年1. 研究產(chǎn)品數(shù)據(jù)模型的輕量化表示理論和方法、數(shù)據(jù)壓縮理論和策略。2. 研制模型格式轉(zhuǎn)換工具集、模型特征的提取分割和復用工具集。3. 整合面向設計過程的建模工具集，進行系統(tǒng)測試4. 研發(fā)設計過程安全保障工具集，進行系統(tǒng)測試5. 大型可信軟件平臺的集成測試及其示范應用。1. 建立統(tǒng)一產(chǎn)品數(shù)據(jù)模型的輕量化表示理論和方法，形成有損和無損的多種有效的數(shù)據(jù)壓縮方案。2. 構(gòu)建幾何算法程序建模與驗證集成平臺原型系統(tǒng)，實現(xiàn)平臺工具集。3. 完成面向設計過程的安全保障工具集4. 形成一個具有原始創(chuàng)新和實用價值的仿真模擬和優(yōu)化設計平臺，在汽車行業(yè)典型產(chǎn)品設計中應用。1