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.