[00148611]框架时序逻辑程序设计

研究成果如下：　　1、创建了完整的投影时序逻辑PTL和命题投影时序逻辑PPTL系统。扩展了区间时序逻辑ITL，在有穷和无穷模型下，严格定义了PTL和PPTL的语法和语义，证明了它们的逻辑规则和相关定理，建立了PTL和PPTL完整的模型理论。基于有穷和无穷模型，建立了PPTL的公理系统并证明了它的合理性和完备性；建立了PTL的公理系统，并证明了它的合理性。　　2、解决了PPTL的判定性，表达性和复杂性问题。　　（1）PPTL的判定性问题：证明了PPTL的可判定性，给出了一个判定算法。特别是，解决了PPTL公式在无穷模型下的判定问题；由于PPTL是PITL的扩展，所以该算法也解决了PITL在无穷模型下长期悬而未决的判定问题。　　（2）PPTL的表达性问题：在国际上首次证明了PPTL的表达能力等价于Buchi自动机，因而证明了PPTL和PITL具有Omega完全正则表达能力。　　（3）PPTL的复杂性问题：以色列学者Kozen在与Moszkowski的个人通讯中非形式地说明了PITL的复杂性下界是非基本的（non-elementary）。我们首次系统地、形式化地证明了PPTL和PITL的复杂性都是严格非基本的。　　3、创建了框架时序逻辑程序设计语言MSVL。以Tempura语言为基础，建立了一个集建模、仿真及验证为一体的框架时序逻辑程序设计语言MSVL。该语言增加了框架操作符，投影操作语句；实现了结构化程序设计语句（顺序，分支和循环语句），时序和并行语句，非确定语句。研究了该语言的模型语义，操作语义和公理语义。　　4、开创了基于PPTL和PITL的模型检测技术。基于PPTL和PITL的判定算法，提出了相应的模型检测算法，开发了相应的模型检测器。　　5、开发了相应的支持工具。包括：框架时序逻辑程序设计语言 -- MSVL 解释器；基于SPIN的模型检测器；基于MSVL的统一模型检测器；基于PVS的定理证明器；HP2P（Hierarchical Hybrid P2P）；Web Services 支持环境 Service Computing and Management Platform（SCMP）；支持FPGA的嵌入式系统测试和验证工具。　　6、应用领域。我们将上述理论和方法应用于实时混合系统、互联网计算和互联网软件如P2P和Web服务以及嵌入式系统的建模和验证。　　该项目在诸多方面取得了突破性进展，有些成果属世界先进水平，得到了国内外同行的肯定。2009年2月14日，国家自然科学基金委员会信息科学部在广州组织有关专家，对该项目进行了验证，专家组一致同意通过该项目验收，并评为优秀。　　课题组共发表论著103篇（部），其中专著2部，编著 4部，国际期刊论文19篇，重要国际会议论文49篇，国内期刊论文28篇，Newcastle大学技术报告（博士论文）1部，特邀报告2次。被SCI收录15篇，EI收录80篇。其中SCI学术它引20次，Google Scholar学术引用169次，CNKI中文引用6次。项目负责人段振华教授博士论文（2006年正式发表于科学出版社英文专著）被相关领域内著名学者多次引用。项目期间申请国家发明专利4项（已获准1项），获软件著作权5项。