File Exchange

## Tabular Expression Toolbox

version 1.23.0.0 (1.75 MB) by Colin Eles

### Colin Eles (view profile)

A tool for creating tabular expressions in Matlab/Simulink integrating checking with PVS and CVC3.

Updated 26 Apr 2015

Tabular Expression Toolbox
Tabular Expressions (also called "tables") provide a precise and concise way to represent mathematical conditional expressions. Tables have been shown to be useful in the documenting and analysing of software systems. The graphical layout of tabular expressions allow for unambiguous interpretation and intuitive inspection of table correctness.
In order for a table to be considered proper it must satisfy two properties, disjointness (no two conditions are true at the same time) and completeness (there is at least one condition that is true.) Tabular expressions have been used on numerous industrial projects, including safety critical applications.
We present a Tabular Expression Toolbox for Matlab/Simulink. The toolbox provides a graphical interface for the creation and manipulation of tabular expressions. The tool allows for the checking of completeness and consistency of tables by leveraging the power of the PVS theorem prover and/or the SMT solver CVC3. By generating a PVS theory of the expression, and using the PVS proof system, we can prove that a table is both disjoint and complete. CVC3 can be used in a similar manner to PVS. For failed proofs the tool will attempt to generate a counter example, which will clearly show to the user why their table is not proper. We provide support for both these tools as they are based on different technologies and therefore have different strengths and weaknesses which we can take advantage of. In order to get the maximum utility of the toolbox we recommend installing both tools. We feel this Table Toolbox brings some needed formalism to Simulink models.

We now support proving tables using floating point types in PVS. See documentation for more details.

The Table Toolbox contains a Simulink block, which when opened allows for the editing of a tabular expression, upon saving a table, the block's inputs and outputs are updated while generating Embedded Matlab Code equivalent to the tabular expression.

The tool will also run from the Toolbox menu in Matlab, allowing users to create tables, check them, then generate an m-file equivalent to the table. The tools will work without having PVS or CVC3 installed on users machine, however they will not be able to automatically check that a table is proper.

Features:
* Integration with PVS theorem prover
* Integration with CVC3 SMT Solver
* Graphical Counter Example Generation
* 1-Dimensional and 2-Dimensional Tables
* Nested headers along vertical dimension
* single output or multiple output
* Compatibility with code generation
* Prove tables with floating point inputs

For installation instructions see README.txt

See included Help files for more information on using the tool.

New features, additional documentation, and bug fixes will continue to be released. Any comments and bugs are welcomed.

References for Tabular Expressions:
C. Eles and M. Lawford, "A tabular expression toolbox for Matlab/Simulink," NASA Formal Methods, LNCS Vol. 6617, pp. 494-499, Springer, 2011.

Y. Jin, D. L. Parnas, Defining the meaning of tabular mathematical expressions, Science of Computer Programming(2010), doi:10.1016/j.scico.2009.12.009

Janicki, R., Parnas, D. L., and Zucker, J. Tabular representations in relational documents. In in Relational Methods in Computer Science (1996), Springer Verlag, pp. 184–196.

Parnas, D.L., Tabular Representation of Relations, CRL Report 260, McMaster University, Communications Research Laboratory, TRIO (Telecommunications Research Institute of Ontario), October 1992, 17 pgs.

A Tabular Expression Toolbox for Matlab/Simulink by Colin Eles

Work supported by the McMaster Centre for Software Certification (http://www.mcscert.ca)

Report bugs to https://groke.cas.mcmaster.ca/gitlab/tables/tet/issues

### Cite As

Colin Eles (2019). Tabular Expression Toolbox (https://www.mathworks.com/matlabcentral/fileexchange/28812-tabular-expression-toolbox), MATLAB Central File Exchange. Retrieved .

Curtis Milo

Mark Lawford

### Mark Lawford (view profile)

Version 0.4.1 addresses problems with Matlab R2011a release. I've got the toolbox working with PVS 5.0 and CVC3 2.2 on Linux (Fedora 15).

Billy

### Billy (view profile)

I'm having a lot of trouble in trying to get this toolbox to operate efficiently on Matlab r2011a. Namely: there are a fair amount of uicontrol callback problems whenever I use the GUI to create the tabular modules. I followed the instructions to the letter and added all of the files to the matlab path. The smt solvers are both accessible by matlab.

solvers being used: cvc3 2.2 and pvs5- allegro

Erdal Bizkevelci

### Erdal Bizkevelci (view profile)

 26 Apr 2015 1.23.0.0 Version 0.7.4 - Initial release for MATLAB R2014b/R2015a. 13 Aug 2014 1.22.0.0 Version 0.7.3 - Fixed a critical bug related to creating new variables. It is recommend to re-save all tables to fix any issues. Please see http://goo.gl/mzq7os for details. 2 Jun 2014 1.21.0.0 Version 0.7.2 - Modify the saving process to provide a stable on disk format. Now when tables are saved, the Simulink Model will not change if the table itself is unmodified. This format is fully compatible with previous versions. 16 Dec 2013 1.20.0.0 Version 0.7.1 - Fixed a bug that occurred when opening tables that prevented the tool from working correctly and prevented Matlab from exiting. 9 Aug 2013 1.19.0.0 Version 0.7 - Updated to support PVS 6.0. Bug fixes for Linux version to handle issues with Matlab including older versions libstdC++ and other shared libraries. Tested with MATLAB R2011b through to R2013a. 20 Jul 2012 1.18.0.0 Version 0.6 - Numerous bug fixes including a severe bug that prevented the user from opening a saved table. 10 Jan 2012 1.17.0.0 Updated to version 0.5, fixed compatibility issues with Matlab 2011b. 23 Aug 2011 1.15.0.0 Updated to support Matlab R2011a, PVS 5.0 and minor documentation updates. 17 May 2011 1.12.0.0 Added support for PVS 5.0 14 Apr 2011 1.11.0.0 Added support for type checking floating point numbers using the NASA PVS library, updated documentation. Minor bug fixes 5 Jan 2011 1.9.0.0 v0.3.1 minor bug fixes, update recommended if using cvc3. 20 Dec 2010 1.8.0.0 Slight modification to the Description. 16 Dec 2010 1.7.0.0 V0.3 adds support for CVC3 a model checker which can be used in place of or along side pvs. Additional documentation is provided, there have been changes to the interface generalizing some of the wording, as well as many bug fixes. 12 Oct 2010 1.6.0.0 Updated help files; added new mode to use Simulink typing, rather than PVS typing, when proving tables; some bug fixes. 24 Sep 2010 1.5.0.0 shouldn't have zipped with OS X 24 Sep 2010 1.4.0.0 Removed some unneeded files
##### MATLAB Release Compatibility
Created with R2015a
Compatible with any release
##### Platform Compatibility
Windows macOS Linux
##### Acknowledgements

Inspired by: statusbar