Better Development of Safety Critical Systems: Chinese High Speed Railway System Development Experience Report 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 searchbased modeldriven 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 modeldriven safety critical software development method.

Prema: A Tool for Precise Requirements Editing, Modeling and Analysis We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet usersu0027 expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well interrelated. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https:youtu.beBX0yv8pRMWs.