一句话：提出 Prema 工具，统一支持形式化需求的编辑、建模与严格验证/确认，并以列车自动防护系统需求为例演示。
需求描述不精确且验证工具之间缺乏互操作性，会导致需求错误难以及早发现。Prema 面向精确需求工程，允许用户用形式化记法编写需求，并通过解析形式建模语言得到准确刻画需求的模型。工具集成了多种严格验证与确认技术，用于检查需求是否符合用户期望并发现潜在错误，从而在同一环境中完成需求编写与验证，避免使用彼此关联松散的多种工具。作者以中国最大的铁路信号控制系统厂商 CASCO 的列车自动防护（ATP）系统需求为案例进行实验演示。由于项目商业保密，工具代码未公开，但提供了演示视频。
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 users' 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 inter-related. 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.be/BX0yv8pRMWs.
@inproceedings{paperbot5298,
title = {Prema: A Tool for Precise Requirements Editing, Modeling and Analysis},
author = {Yihao Huang and Jincao Feng and Hanyue Zheng and Jiayi Zhu and Shang Wang and Siyuan Jiang and Weikai Miao and Geguang Pu},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00128}
}