A Tabular Expression to Event-B Language Transformation Tool

Abstract

Tabular expressions have been proved in practice to be an excellent way to check the completeness (all possibilities are considered) and disjointness (no overlap among conditions) of software requirements described as functions. However, just these two properties alone are not sufficient for justifying the safety and efficacy of safety critical systems. Formal specification languages like Z, CSP and Event-B can also support mathematical reasoning required for these kinds of systems and have more effective tool support available. This thesis reports on a new transformation tool TX2EB (Tabular Expressions to Event-B) which combines the completeness and disjointness checks and mathematical reasoning needed for verification and classification of the documented requirements. Moreover, the proposed tool can generate formal specifications from the tabular expressions automatically and support subsequent refinement and analysis of the specifications. Therefore, it can liberate researchers from tedious and time-consuming manual application of the transformation.