(1)建立了完整的投影时序逻辑PTL和命题投影时序逻辑PPTL系统。建立了PTL和PPTL的模型理论，包括100多个定理和500多个逻辑规则。建立了命题投影时序逻辑PPTL的公理系统，包含28条公理和6条推理规则。建立了命题投影时序逻辑PPTL的可判定性、复杂性和表达性理论。(2)以PTL的可执行子集为基础，设计并开发了集建模、仿真和验证为一体的并行程序设计语言MSVL(Modeling,SimulationandVerificationLanguage)。该语言不但支持C语言的所有程序结构，而且还定义了框架操作符frame，解决了时序逻辑语言中经典的框架问题(即变量的值如何从前一个状态保持下来的问题)。实现了变量的内存自动分配和释放，增加了投影操作符prj、过去时序操作符和无穷模型，引入了等待语句和非确定选择语句。给出了该语言的最小模型语义、操作语义和公理语义。证明了它们的一致性。提出了基于MSVL的多核并行程序设计模型。(3)以MSVL为建模语言，PPTL为性质规范语言，建立了一套建模、仿真和验证技术。具体包括：建模与仿真，统一、偏序、符号、限界和抽象模型检测，以及定理证明。(4)给出了C、Verilog、VHDL程序和工作流网到MSVL的转换理论与方法，从而可以使用基于MSVL的验证技术来完成C、Verilog、VHDL程序和工作流网的验证。(5)提出了模型检测状态空间缩减新算法，包括虚假反例路径检测、抽象模型精化、打结不变PLTL公式产生、以及基于Steiner树和贪婪算法的最小联通支配集构造算法。(6)开发了支持上述形式化方法的建模、仿真和验证工具集MSV。该工具集支持MSVL程序的编辑与调试，建模、仿真和验证，以及C、Verilog、VHDL程序和工作流网到MSVL程序的自动转换。目前该工具可以支持万行以上的C、Verilog和VHDL到MSVL的自动转换和验证。       在项目资助下，共发表学术论文（著作）200余篇，其中SCI国际期刊论文50余篇，顶级国际会议（ICSE2013，ICLP2005，ATPN2007等）论文10余篇，授权专利3项，获软件著作权8项。截止2014年2月28日，20篇代表作被引用850次（其中他引473次）。项目所取得的成果在有些方面达到了国际领先水平，并得到了区间时序逻辑创始人BenMoszkowski等同行专家和中科院已故唐稚松院士的引用和好评。2009年2月14日和2012年12月11日，国家自然科学基金组织有关专家在广州对国家自然科学基金重点项目《框架时序逻辑程序设计》和国家自然科学基金重大合作项目《构造可信、高效软件系统的基础研究》进行了结题验收，分别评定为优秀。项目的研究成果已成功应用于中国航天科技集团五院502所、中国航天科工集团第二研究院706所、中国电子科技集团第五十八研究所以及陕西多家软件公司所承担的系统的开发和验证中，发现了一些深度隐藏的程序错误，提高了系统的可靠性和正确性，并取得了良好的经济和社会效益。