Theano: A Tool for Verifying the Consistency and Completeness in Tabular Requirements

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.