一句话：分享中国高铁安全关键系统开发挑战，提出用SysML精化与SAT求解检查模型的搜索式模型驱动方法。
安全关键系统的正确性保障是全球软件工程中的关键问题，中国高速铁路系统的软件开发尤其具有挑战。过去数年，作者团队协助中国最大的高速铁路信号企业卡斯柯（CASCO Signal Ltd）开发高速铁路安全关键软件，并贡献了若干具体开发方法。本文报告一种基于搜索的模型驱动软件开发方法：使用SysML图精化方法构建SysML模型，并借助SAT求解器对模型进行检查。报告旨在分享高铁安全关键系统开发中的挑战、从与企业合作开发安全关键软件中获得的经验，并以ZC子系统为案例，展示系统化的模型驱动安全关键软件开发方法。
Ensure the correctness of safety critical systems play a key role in the worldwide software engineering. Over the past years we have been helping CASCO Signal Ltd which is the Chinese biggest high speed railway company to develop high speed railway safety critical software. We have also contributed specific methods for developing better safety critical software, including a search-based model-driven software development approach which uses SysML diagram refinement method to construct SysML model and SAT solver to check the model. This talk aims at sharing the challenge of developing high speed railway safety critical system, what we learn from develop a safety critical software with a Chinese high speed railway company, and we use ZC subsystem as a case study to show the systematic model-driven safety critical software development method.
DOI 原文 ·
@inproceedings{paperbot5337,
title = {Better Development of Safety Critical Systems: Chinese High Speed Railway System Development Experience Report},
author = {ZhiWei Wu and Jing Liu and Xiang Chen},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00143}
}