高可信软件的基础理论研究

作者: 时间:2019-07-30 点击数:

    创建了PTL系统,建立了相关的模型理论和公理系统;证明了PPTL的可判定性,解决了命题区间时序逻辑(PITL)在无穷模型下25年悬而未决的判定问题;证明了PPTL的表达能力是完全正则的,复杂性是非基本的;建立了PTL的公理系统,并开发了相应的定理证明器;设计并实现了基于SPIN的PPTL模型检测器。

     以PTL为基础建立了集建模、仿真和验证为一体的并行程序设计语言MSVL,能有效地支持多核环境下的并行程序设计;定义了MSVL的最小模型语义、操作语义和公理语义;建立了MSVL的公理系统,并开发了相应的定理证明器;开发了MSVL语言的解释器和建模及验证工具MSV;开发了模型驱动的高可信软件支持工具集Hidep。

     基于光滑技术、园搜索技术构造出了可求出高维复杂优化问题全局最优解的高效算法。提出了一个可以求解非线性双层规划问题的进化算法。研究了Deep Web数据集成和挖掘中的一些关键问题,基于无冗余公共子序列图和并行集合链提出了一种新的最长公共子序列(MLCS)算法,彻底解决了MLCS 40年来未解决的难题。

     关于PTL与MSVL的研究成果多次得到区间时序逻辑创始人斯坦福大学的Ben Moszkowski、英国Kent大学的Bowman和Thompson、Rodolfo Sabas Gomez,加拿大滑铁卢大学Peter R. King和Helen Cameron,以及中科院已故唐稚松院士等同行专家的引用和好评。项目组的研究成果已经发表在国际重要学术期刊Theoretical Computer Science、Mathematical Structures in Computer Science与Journal of Combinatorial Optimization等上,所开发的可信软件理论、技术和工具已经成功应用于中国航天科工集团第二研究院706研究所承担的海军某指挥系统的开发中,取得了显著地经济效益,并获得授权专利1项,省部级科研奖1项。

     非线性双层规划问题的进化算法突破了多目标双层规划不能有效求解的关键技术,使得这些问题能有效地解决,与研究同类问题学者相比,该成果具有一定的价值。多目标优化理论及其算法已用于求解实际生活和科学研究中的多目标问题,并取得了较好的效果。任务调度优化模型研究成果已用于三个实际问题:车间作业调度、网格任务调度、云计算任务调度。科研成果已经发表在Computing and Informatics、Applied Mathematics and Computation、INFORMS Journal on Computing,并获得省部级科研奖1项。

该成果的不同部分内容与2009年和2012年分别获陕西省科学技术奖二等奖。