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.
* 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.
See also included presentation:
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
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).
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
Version 0.7.4 - Initial release for MATLAB R2014b/R2015a.
Version 0.7.3 - Fixed a critical bug related to creating new variables. It is
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.
Version 0.7.1 - Fixed a bug that occurred when opening tables that prevented the tool from working correctly and prevented Matlab from exiting.
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.
Version 0.6 - Numerous bug fixes including a severe bug that prevented the user from opening a saved table.
Updated to version 0.5, fixed compatibility issues with Matlab 2011b.
Updated to support Matlab R2011a, PVS 5.0 and minor documentation updates.
Added support for PVS 5.0
Added support for type checking floating point numbers using the NASA PVS library, updated documentation.
Minor bug fixes
v0.3.1 minor bug fixes, update recommended if using cvc3.
Slight modification to the Description.
V0.3 adds support for CVC3 a model checker which can be used in place of or along side pvs.
Updated help files; added new mode to use Simulink typing, rather than PVS typing, when proving tables; some bug fixes.
shouldn't have zipped with OS X
Removed some unneeded files