A Table Checking Tool
Ms. Min Jing
Software is used increasingly in safety critical and mission critical
systems. The software products are required to be reliable and accurate.
Good documentation, especially precise mathematical documentation,
contributes to increasing reliability and accuracy of software products.
Tabular notation advocated by Parnas et al. has been found to be easier
to understand, formulate and inspect than traditional mathematical notations.
The formulae in the tabular expressions must satisfy certain mathematical
conditions. When these tables are used in practice, we have found that the
documents submitted for review often fail to satisfy those conditions.
Manually checking these simple and application-independent properties is
time-consuming and error-prone.
This work involves the design and development of a prototype tool to automate
the table completeness and consistency checking process. The checking is
performed by formulating theorems from a tabular expression and verifying
theorems by using PVS (Prototype Verification System) without human interaction.
It helps the software documentation reviewers to do preliminary checking and can
also be used by other tools when they need to manipulate the domain of the table.