一句话：提出 Theano，自动验证 Simulink Requirements Tables 中表格化需求的一致性与完备性，并以汽车案例演示。
表格化需求通过“if-then”范式规定软件行为。验证这类需求的一致性与完备性至关重要，可发现规格错误、降低开发时间与成本，并预防潜在故障。Theano 是面向 Simulink Requirements Tables 的验证工具，旨在确保表格化需求的一致性与完备性。这篇演示论文介绍 Theano 的关键特性，通过一个汽车案例研究展示其应用，并讨论底层实现与设计选择。作者还提供了在线视频走查：youtu.be/p71bKupmRUQ。
Tabular requirements prescribe software behavior through an "if-then" paradigm. Verifying the consistency and completeness of tabular requirements is crucial, as it can identify specification errors, reduce development time and costs, and help prevent potential failures. Theano is a verification tool designed to ensure the consistency and completeness of tabular requirements formulated with Simulink Requirements Tables. This demonstration paper presents the key features of Theano, illustrates its application through an automotive case study, and discusses the underlying implementation and design choices. An online video walkthrough of the case study is also available: youtu.be/p71bKupmRUQ
@inproceedings{ZanengaBIBGRM25,
title = {Theano: A Tool for Verifying the Consistency and Completeness in Tabular Requirements},
author = {Aurora Francesca Zanenga and Nunzio Marco Bisceglia and Benedetta Ippoliti and Andrea Bombarda and Angelo Gargantini and Akshay Rajhans and Claudio Menghi},
booktitle = {FSE},
year = {2025},
doi = {10.1145/3696630.3728599}
}