时空统一建模、精化和验证方法研究

Unified modeling time and space is the main concern in the construction of the new generation IT systems, e.g., Cyber Physical Systems, Cyberspace, and Mobile Internet Systems. However, due to the features like the mutual causality and dependency between the time info and space info, as well as the continuity and infinity of time and space, we still lack a unified syntax and semantics expression to describe time and space together. The existing modeling mechanisms are not enough for the precise and complete description of the linking between time and space. They cannot support the modeling of multiform time and space, especially the systems where temporal logic and spatial logic are in a non-orthogonal composition way. We aim at studying the approach to modeling the relations between multiform time and multiform space, sorting out solutions to key issues including unified spatial temporal models construction, relational model development of time and space, model refinement, verification of correctness, consistency guarantee. We will establish a framework that supports hierarchical modeling and step wise refinement. And we will provide mechanisms to guarantee the consistency in both vertical and horizontal dimensions. We will provide a method to precisely analyze the traces of a system to improve the predictability of a system. A Unified Spatio Temporal Modeling Environment will be developed to support model construction, refinement, simulation and verification. Then the research results will be applied to develop China trustworthy train control system iCMTC, and hope we can make contribution to high safety software R&D nationalization.

时空统一建模是信息物理系统、赛博空间、移动互联系统等新一代信息系统，以及时间空间攸关的高安全系统构造中的核心问题。但由于时空信息互相依赖、互为存在条件以及时空的连续性、无限性等特点，目前缺乏精确、全面描述时空特性及时间与空间关联性的模型，缺乏统一的时空语法、语义表达。不能有效支持多形态时间空间系统建模，特别是时间逻辑与空间逻辑非正交结合系统。本项目研究在多形态时间关系、多形态空间关系基础上的时空统一建模方法，探索解决时空模型构造、时空关联建模、模型精化、正确性验证、一致性保障几个关键问题。建立一套层次化建模和逐步精化的模型精化体系，并保证模型系统的纵向一致性和横向一致性。给出精准分析系统的行为轨迹的方法，提高系统行为可控性。开发时空统一建模环境，为模型构造、精化、仿真、验证提供全方位支持，最后将研究成果应用于国产可信轨交列控系统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检索”的指标。