 |
| |
实验室介绍: |
|
清华信息科学与技术国家实验室（筹）中法软件系统建模验证联合实验室于2010年12月正式成立，由清华大学软件学院、计算机系和法国Verimag研究所联合成立，其目标是以中国工业界的实际需求为对象，在软件验证技术、基于构建的嵌入式系统设计、混成系统设计与验证和嵌入式系统编程语言及开发环境等方面开展深入研究，为中国工业界开发出可用的嵌入式软件验证工具，在国际学术界形成一个新的流派，使清华大学在这一领域处于世界一流水平，并建立一支世界一流的研究团队，将实验室建成国际嵌入式软件验证的学术中心和为工业界提供技术和工具的验证服务中心。
联合实验室主任由国际嵌入式领域著名学者、2007年图灵奖获得者Joseph Sifakis教授和清华信息科学与技术国家实验室（筹）主任孙家广院士共同出任。 |
研究方向：
|
 软件验证技术：面向嵌入式软件领域，基于模型检测和定理证明技术分别对模型级和代码级软件进行验证。针对嵌入式软件的实时、资源受限、反应式等特征，开发有效的模型检测算法和证明策略，以有效提高验证的规模和速度；同时，研究模型检测和定理证明的有效结合方法，以便取长补短，满足工业验证需求。
|
基于构件的嵌入式系统设计：着重研究基于构件的嵌入式系统设计方法，包括嵌入式系统设计的形式建模技术、代码生成技术以及模型转换正确性保证方法等。其中，寻找或开发合适的形式建模语言以及嵌入式系统建模方法学，以便对既包含软件又包含硬件的嵌入式系统在适当的粒度进行精确建模，是研究的重点。
|
混成系统设计与验证：将针对嵌入式系统的混成特征，研究混成系统的设计和验证方法，包括选择适当的数学逻辑和形式语言对混成系统进行建模、选择适当的验证方法对混成系统进行有效验证、对设计和验证问题进行有效分解以及开发有效的混成系统验证算法，使其能够处理工业级应用规模等。
|
嵌入式系统编程语言及开发环境：将致力于研究新一代的嵌入式系统编程语言及其开发环境，通过提供包含领域知识语义的已验证组件，减轻开发负担，并自动保证局部正确性；通过将多种分析方法和工具集成到开发环境中，在编程语言层面进行多种形式验证，能够进行主动检查以及警告信息提醒，以有效辅助开发人员提高嵌入式系统的开发效率和可靠性。
|
联合实验室团队构成: |
主任： |
Joseph Sifakis
法国国家科学研究院研究总监
清华大学软件学院 客座教授
研究方向：嵌入式系统验证，模型检查(Model-Checking)
个人主页：暂无
|
|
孙家广
清华大学信息科学与技术学院 院长
清华信息科学与技术国家实验室 主任
中国工程院 院士
研究方向：软件工程、图形学
个人主页：暂无
|
|
主要成员： |
顾明
清华大学软件学院 教授
研究方向：可信软件
个人主页：暂无
|
|
罗贵明
清华大学软件学院 教授
研究方向：系统辨识、软硬件系统的形式化验证、模型检测
个人主页：暂无
|
|
李春平
清华大学软件学院 副教授
研究方向：人工智能，知识处理及推理技术，数据和文本挖掘，Web信息资源搜索，文档自动分类
个人主页：暂无
|
|
张宏宇
清华大学软件学院 教授
研究方向：计算机网络及应用
个人主页：暂无
|
|
荔建琦
清华大学软件学院 博士后
研究方向：形式化方法、定理证明和程序验证
个人主页：暂无
|
|
贺飞
清华大学软件学院 讲师
研究方向：模型检测的基础理论与算法实现、组合优化算法设计与分析
个人主页：暂无
|
|
陈渝
清华大学计算机系 副教授
研究方向：操作系统，普适计算，嵌入式系统
个人主页链接
|
|
白晓颖
清华大学计算机系 副教授
研究方向：软件工程中的软件质量工程、软件测试、服务计算
个人主页：暂无
|
|
董渊
清华大学计算机系 副教授
研究方向：操作系统、编译器构造和基于语言的安全、嵌入系统
个人主页链接
|
|
王生原
清华大学计算机系 副教授
研究方向：程序设计语言与系统、并发系统建模、Petri网理论与应用
个人主页：暂无
|
|
JOUANNAUD Jean-Pierre
法国国家信息与自动化研究所（INRIA）高级研究员
中法信息、自动化与应用数学联合实验室(LIAMA)法方主任
研究方向：形式化方法、定理证明和程序验证
个人主页：暂无
|
|
Joloboff Vania
法国国家信息与自动化研究所（INRIA）研究员
研究方向：嵌入式软件、混成系统、非线性控制
个人主页：暂无
|
|
BLANQUI Frederic
法国国家信息与自动化研究所（INRIA）研究员
研究方向：嵌入式系统
个人主页：暂无
|
|
Monin Jean-francois
法国CNRS资深研究员，格勒诺布尔第一大学教授
研究方向：定理证明
个人主页：暂无
|
|
张荷花
法国国家信息与自动化研究所（INRIA）博士后
研究方向： 可信软件
个人主页：暂无
|
|
|
|
|
|
.jpg){kind=small}
