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

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

项目编号： No.61370100

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 陈仪香

作者单位： 华东师范大学

项目金额： 73万元

中文摘要： 软件形式化方法是软件工程科学重要方法，研究成果对程序语言设计、软件实现具有重要指导意义。本项目针对当前软件领域中诸如物联网、信息物理融合系统（CPS）以及云计算等研究热点所涉及到的实时智能体在任务处理方面呈现时空一致性科学问题展开系统基础研究和仿真验证。在已有研究工作基础上，建立能反映系统与智能体时空一致性的软件形式化模型，具体包括完善描述软件系统时空一致性的程序规范语言（STeC），建立时间和空间驱动的时空自动机模型以及基于时钟（Clock）的时钟逻辑系统，在形式化模型基础上，设计具有时空一致性的智能体及系统的体系结构以及评估和分析方法，构建STeC+Matlab/Similink仿真验证平台，分析和验证本项目建立的形式化模型以及体系结构设计的合理性与有效性。研究成果既丰富软件工程的基础理论，又为当前信息技术提供技术支撑。本项目研究具有学术前沿性和创新性，具有重要理论意义和实际应用价值。

中文关键词： 软件形式化方法；软件形式化模型；时空一致性；程序规范语言；时空自动机模型

英文摘要： 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 reseac

英文关键词： Formalization Method of Software；Formalization Model of Software；Spatial-Temperal Consistence；Programming Specification Language；Model of Temporal-Spatial Automata