《多類型時序邏輯程式設計》是依託西安電子科技大學，由趙亮擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：多類型時序邏輯程式設計
- 項目類別：青年科學基金項目
- 項目負責人：趙亮
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
時序邏輯程式設計是目前一種廣泛使用的程式設計模式，對程式驗證具有重要的意義。本項目擬研究多類型時序邏輯程式設計，以加強時序邏輯程式設計的功能和適用性。為此，我們在建模、仿真和驗證語言（MSVL）的基礎上引入類型的概念，並定義多種類型，得到一種多類型時序邏輯程式設計語言：多類型MSVL。研究多類型MSVL的類型系統、模型語義、操作語義、公理語義、類型安全性和語義之間等價性。開發多類型MSVL的解釋器，實現對多類型時序邏輯程式的類型檢查、建模、仿真和驗證。
結題摘要
時序邏輯程式設計是目前一種廣泛使用的程式設計模式，對程式驗證具有重要的意義。現有的時序邏輯程式設計語言注重在邏輯方面的功能，然而在類型方面的功能有限，往往僅支持單一類型。本項目對建模、仿真和驗證語言MSVL進行擴展，使用投影時序邏輯PTL定義了整型、浮點型、字元型、數組、列表、指針、結構等多種類型以及各類型的相關操作，得到了一種多類型的時序邏輯程式設計語言。構建了多類型MSVL的形式語義理論體系，以極小模型的方式定義了該語言的模型語義，以格局約簡的方式定義了該語言的操作語義，並證明了這兩種語義的等價性。研究了基於PTL的程式驗證理論，提出了相應的模型檢測方法和運行時驗證方法。作為理論的實現，開發出多類型MSVL的解釋器工具，具備對多類型時序邏輯程式的建模、仿真與驗證功能。作為理論和工具的套用，實現了一種基於多類型MSVL的社交網路系統驗證方法，並使用該方法驗證了社交網路系統中若干條關於隱私策略和用戶關係強度的性質。本項目對多類型MSVL的開發與研究改進了目前國內外時序邏輯程式設計語言缺乏多類型支持這一不足，增強了時序邏輯程式設計的功能和適用性。
