科研成果速递！上海市高可信计算重点实验室杜德慧教授团队两项科研成果被软件工程领域顶级国际会议录用

近期，上海市高可信计算重点实验室杜德慧教授团队设计、开发的新型CPS系统仿真建模及验证工具，解决了开放环境下智能CPS系统可信建模及验证难题！此外，该团队提出的自动驾驶建模语言SML4ADS及可视化建模工具，支持建模自动驾驶的各种场景，并集成仿真、验证技术，实现场景的仿真及验证。以上两项科研成果分别被软件工程领域的顶级国际会议ASE2022 tool DEMONSTRATION和ASE2022 LBR录用！

一：

针对ICPS的可信建模及验证面临的挑战性问题，该团队设计、开发了RoboSimVer用于建模和分析RoboSim仿真模型。该工具平台的框架如图所示：RobosimVer实现了一种基于模式和映射规则的模型转换方法，将RoboSim模型转换为等价的时间自动机网络(Network of time Automata)进行验证分析。

图1 RoboSimVer技术框架

该项研究与英国约克大学计算机学院Ana Cavalcanti教授合作。实验室杜德慧教授为第一作者完成的相关研究成果，以“RoboSimVer: A Tool for RoboSim Modeling and Analysis”为题发表在第37界“IEEE/ACM International Conference on Automated Software Engineering（ASE）”（CCF A类会议），论文录用链接：https://conf.researchr.org/track/ase-2022/ase-2022-tool-demonstrations?#event-overview。

二：

基于验证技术的场景分析，可以降低场景测试的成本，并快速识别出安全攸关的场景。然而，现有的场景描述方法不支持应用形式化验证的技术对场景中的车辆行为进行验证分析。针对以上问题，团队设计并实现一种面向自动驾驶场景的领域特定建模语言SML4ADS，并提出一套通用的场景仿真框架，将抽象的场景模型转化为CARLA 自动驾驶仿真器中可执行的具体场景。此外，使用形式化验证工具UPPAAL SMC对SML4ADS场景模型中的车辆行为进行验证与分析。

图2 自动驾驶场景建模及验证

实验室硕士研究生李博为第一作者、杜德慧教授为通讯作者完成的研究成果，以“SML4ADS: An Open DSML for Autonomous Driving Scenario Representation and Generation”为题，发表在ASE2022（CCF A类会议），论文录用链接：https://conf.researchr.org/track/ase-2022/ase-2022-late-breaking-results?#event-overview。