TITLE: A Tabular Expression Toolbox for Matlab/Simulink

ii Model based design has had a large impact on the process of software develop-ment in many different industries. A lack of formality in these environments can lead to incorrect software and does not facilitate the formal analysis of created models. A formal tool known as tabular expressions have been suc-cessfully used in developing safety critical systems, however insufficient tool support has hampered their wider adoption. To address this shortfall we have developed the Tabular Expression Toolbox for Matlab/Simulink. We have developed an intuitive user interface that allows users to easily create, modify and check the completeness and disjointness of tabular expres-sions using the theorem prover PVS or SMT solver CVC3. The tabular expres-sions are translated to m-functions allowing their seamless use with Matlab’s simulation and code generation. We present a method of generating counter examples for incorrect tables and a means of effectively displaying this infor