具有時空一致性的軟體形式化理論與方法的研究

《具有時空一致性的軟體形式化理論與方法的研究》是依託華東師範大學，由陳儀香擔任項目負責人的面上項目。

基本介紹

• 中文名：具有時空一致性的軟體形式化理論與方法的研究
• 項目類別：面上項目
• 項目負責人：陳儀香
• 依託單位：華東師範大學

項目摘要

軟體形式化方法是軟體工程科學重要方法，研究成果對程式語言設計、軟體實現具有重要指導意義。本項目針對當前軟體領域中諸如物聯網、信息物理融合系統（CPS）以及雲計算等研究熱點所涉及到的實時智慧型體在任務處理方面呈現時空一致性科學問題展開系統基礎研究和仿真驗證。在已有研究工作基礎上，建立能反映系統與智慧型體時空一致性的軟體形式化模型，具體包括完善描述軟體系統時空一致性的程式規範語言（STeC），建立時間和空間驅動的時空自動機模型以及基於時鐘（Clock）的時鐘邏輯系統，在形式化模型基礎上，設計具有時空一致性的智慧型體及系統的體系結構以及評估和分析方法，構建STeC+Matlab/Similink仿真驗證平台，分析和驗證本項目建立的形式化模型以及體系結構設計的合理性與有效性。研究成果既豐富軟體工程的基礎理論，又為當前信息技術提供技術支撐。本項目研究具有學術前沿性和創新性，具有重要理論意義和實際套用價值。

結題摘要

本項目自2013年立項以來，一直圍繞項目的研究計畫和內容進行開展研究。以信息領域中諸如物聯網、信息物理融合系統、高速運動等安全攸關領域研究熱點為研究背景，展開實時智慧型系統時空一致性的形式化規範模型研究。在系統的需求層對時空約束需求進行規範建模、設計和驗證這個具有挑戰性的研究領域取得了系統的具有影響的研究成果。 本項目研究具有時空一致性的軟體形式化理論與方法，完善了描述軟體系統時空一致性的程式規範語言（STeC），建立了時間和空間驅動的時空自動機模型以及基於時鐘（Clock）的時鐘邏輯系統，在形式化模型基礎上，設計具有時空一致性的智慧型體及系統的體系結構以及評估和分析方法，構建STeC+Matlab/Similink/UPPAAL仿真驗證平台，分析和驗證本項目建立的形式化模型以及體系結構設計的合理性與有效性。 獲得的重要結果有：1、具有時空一致性的系統需求規範語言STeC的研究： 建立了STeC的UTP精化語義模型以及基於STeC的時空自動機模型；擴展STeC，建立了機率化的STeC規範語言PSTeC以及參數化的STeC規範語言PSTeC,擴展後的STeC可以用來規範不確定環境的實時系統時空一致性約束；設計了從STeC到Maude、Matlab/Simulink以及時間自動機UPPAAL的轉換規則和方法，構建了STeC設計和分析驗證工具平台。 2、時鐘邏輯系統研究：提出了一種適用於分散式系統通信的新模型Timed-pNets；建立了基於STeC-CCSL建模技術的驗證理論以及與STeC相關的混成時鐘邏輯系統。3、具有時空約束的系統的研究：建立了一種面向車聯網系統的具有時空約束的事件驅動體系結構； 針對車聯網中時空事件流的處理問題，提出了基於Petri網的處理模型。4、物聯網中典型問題研究：針對物聯網中的無線網路感測器（WSN），提出了一種置信度模型；結合軟硬體協同的思想，給出了一種面向無線網路感測器(WSN)系統的設計與實現方法；設計了一種基於車速的自適應交通信號燈控制系統。5、增加了非經典進程代數模擬和互模擬的研究：建立了資源供需進程的跡等價關係和互模擬關係以及系統的互模擬及其邏輯基礎。 本項目研究成果既豐富了軟體工程的基礎理論體系和方法，又為物聯網、信息物理融合系統以及高速運動等信息技術研究熱點提供理論和技術支撐，具有重要的理論意義和實際套用價值。