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 Table 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 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.
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) |
