Code covered by the BSD License  

Highlights from
Tabular Expression Toolbox

4.0

4.0 | 1 rating Rate this file 40 Downloads (last 30 days) File Size: 1.76 MB File ID: #28812
image thumbnail

Tabular Expression Toolbox

by

 

23 Sep 2010 (Updated )

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

| Watch this File

File Information
Description

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.

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)

Acknowledgements

Statusbar inspired this file.

Required Products Simulink
MATLAB release MATLAB 8.1 (R2013a)
Other requirements * Tested with MATLAB 2012a, 2011a. * PVS (optional) download from http://pvs.csl.sri.com/ PVS is only available for OS X and UNIX. * CVC3 (optional) download from http://cs.nyu.edu/acsys/cvc3/ CVC3 Available for OS X, Linux, and Windows
Tags for This File   Please login to tag files.
Please login to add a comment or rating.
Comments and Ratings (3)
24 Aug 2011 Mark Lawford

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

09 Jun 2011 Billy

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

10 Mar 2011 Erdal Bizkevelci  
Updates
24 Sep 2010

Removed some unneeded files

24 Sep 2010

shouldn't have zipped with OS X

12 Oct 2010

Updated help files; added new mode to use Simulink typing, rather than PVS typing, when proving tables; some bug fixes.

16 Dec 2010

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.

20 Dec 2010

Slight modification to the Description.

05 Jan 2011

v0.3.1 minor bug fixes, update recommended if using cvc3.

14 Apr 2011

Added support for type checking floating point numbers using the NASA PVS library, updated documentation.

Minor bug fixes

17 May 2011

Added support for PVS 5.0

23 Aug 2011

Updated to support Matlab R2011a, PVS 5.0 and minor documentation updates.

10 Jan 2012

Updated to version 0.5, fixed compatibility issues with Matlab 2011b.

23 Jul 2012

Version 0.6 - Numerous bug fixes including a severe bug that prevented the user from opening a saved table.

09 Aug 2013

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.

17 Dec 2013

Version 0.7.1 - Fixed a bug that occurred when opening tables that prevented the tool from working correctly and prevented Matlab from exiting.

02 Jun 2014

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.

Contact us