《時空統一建模、精化和驗證方法研究》是依託華東師範大學，由劉靜擔任項目負責人的面上項目。
基本介紹
- 中文名：時空統一建模、精化和驗證方法研究
- 項目類別：面上項目
- 項目負責人：劉靜
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
時空統一建模是信息物理系統、賽博空間、移動互聯繫統等新一代信息系統，以及時間空間攸關的高安全系統構造中的核心問題。但由於時空信息互相依賴、互為存在條件以及時空的連續性、無限性等特點，目前缺乏精確、全面描述時空特性及時間與空間關聯性的模型，缺乏統一的時空語法、語義表達。不能有效支持多形態時間空間系統建模，特別是時間邏輯與空間邏輯非正交結合系統。本項目研究在多形態時間關係、多形態空間關係基礎上的時空統一建模方法，探索解決時空模型構造、時空關聯建模、模型精化、正確性驗證、一致性保障幾個關鍵問題。建立一套層次化建模和逐步精化的模型精化體系，並保證模型系統的縱向一致性和橫向一致性。給出精準分析系統的行為軌跡的方法，提高系統行為可控性。開發時空統一建模環境，為模型構造、精化、仿真、驗證提供全方位支持，最後將研究成果套用於國產可信軌交列控系統iCMTCt的研發，力爭為我國高安全軟體自主研發做出貢獻。
結題摘要
本課題從時空統一建模和提高時空模型精度入手，針對時空信息互相依賴、互為存在條件以及時空的連續性、無限性的特點, 研究精確、全面的時空語義表達，並在多形態時間系統與空間系統的基礎上，建立離散/稠密時空模型，分析時空約束強度、並存與優先權描述，研究了複雜約束條件下的描述與驗證方法，建立了統一的時空模型。統一描述多視角多層次模型，給出模型精化策略和保證模型正確性、一致性的方法與以適應強時空系統設計。開發了建模與分析驗證支持工具，並和卡斯柯信號有限公司合作將研究成果與工具套用到新一代基於車車通信的軌道交通列控系統試驗線中。 本課題組在計算機軟體理論領域國際權威期刊、重要學術會議、國內一級學報上發表論文33篇（含已接收），專利申請已接受3項，軟體著作權3項。其中國際期刊《IEEE Transactions on Intelligent Transportation Systems》和《Mathematical Problems in Engineering》上等發表9篇學術論文，在《IEEE Real-Time Systems Symposium (RTSS)》和《IEEE/ACM International Conference on Automated Software Engineering (ASE)》等國際學術會議上發表論文22篇，其中CCF A類/SCI 一區 4篇, 其它論文均屬SCI/EI/ISTP收錄源；已出版的學術論文共28篇，專利申請已接收3項，軟體著作權3項；承辦國內外學術會議3次；課題組長和主要課題組成員擔任重要國際學術會議程式委員會委員 (PC Member) 10次, 邀請海外同行專家進行學術交流12人次；參加境外學術會議8人次。各項指標都大大超過項目申請時“預計有20篇的學術論文公開發表，其中至少有10篇被SCI或EI檢索”的指標。
