具有时空一致性的软件形式化理论与方法的研究

Software Formal Methods is an important method of software engineering science. Study on it will have important guiding singnificance on both the design of programming language and the implementation of software. The project will focus on the basic reseach and simulation of the spatial and temporal consistency of intelligent tasking system appeared in the current research-hot-fields of software engineering, such as the internet of things, cyber-physical system as well as cloud computing. On the basis of the existing research work, this project will establish the software formal model to reflect the spatial and temparol consistence of the system with the intelligent body, including:(1) to perfect the description of spatial-temporal consistency specification language (STeC),(2)to establish the driven-spatial&temparolautomatic machine model and the clock logic system,(3) to design the architecture and evaluation and analysis methods for agent and system with the spatial-temperol consistence on the basis of the formal model,(4) to build STeC + Matlab / Similink simulation platform to analysis and verify the rationality and effectiveness of the formal model and architecture design to be established in this project. Research results of this project not only enrich the basic theory of software engineering and also provide technical support for the current information technology. This project has the academic cutting-edge and innovative as well as important theoretical significance and practical value.

软件形式化方法是软件工程科学重要方法，研究成果对程序语言设计、软件实现具有重要指导意义。本项目针对当前软件领域中诸如物联网、信息物理融合系统（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、增加了非经典进程代数模拟和互模拟的研究：建立了资源供需进程的迹等价关系和互模拟关系以及系统的互模拟及其逻辑基础。.本项目研究成果既丰富了软件工程的基础理论体系和方法，又为物联网、信息物理融合系统以及高速运动等信息技术研究热点提供理论和技术支撑，具有重要的理论意义和实际应用价值。