基于模型的可信软件理论与方法

基于时钟语言的需求建模理论与方法：

1.在国际上首次提出了具有时间性质的问题框架建模方法，支持实时系统中的时钟关系描述，活性和安全性等性质的分析与验证。

实现了一种结合时空特征的UML模型的开发技术

设计模型的一致性分析与检测方法：

1.创新地提出了支持模型语义一致性检查的方法，验证了商业流程模型的操作语义与代数语义的一致性。

提出了统一的描述与验证XML约束的方法，有效地解决了约束逻辑公式相对于树模型的可满足性验证问题

模型驱动的测试技术：

1.针对基于系统高阶规约测试用例的效率问题，首次提出了基于SystemC错误模型自动产生属性的方法。

给出了一套有效的PSL断言与测试用例转化规则，创新性地实现了系统顶层规约与底层实现间验证结果的重用，减少了测试用例生成的时间

资源受限场景设计模型的自动综合：

1.创造性地提出了多种有效约减设计空间的方法。

开发的基于多核平台的综合工具将高阶综合的速度提升了10倍以上，达到国际领先水平

成果：

1.基于模型的可信软件理论与开发方法的成果获2011年教育部自然科学一等奖；

2.在高水平国际期刊和会议上累计发表论文40余篇。

Springer出版的英文专著1部