Tabster is a java object oriented library designed for verifying critical properties of tabular expressions through the use of SMT solvers. When a given property is not satisfied, Tabster returns counter examples to highlight the situation in which the property fails to hold. Download the latest version from here.
Tabular Expressions
When designing software for mission critical systems, developers often need to clearly determine what output a program should give for different classes of inputs. As it turns out, tables provide a clear and convenient way to communicate these conditions and have been used successfully in the development of embedded and safety critical systems. They allow for easier readability of documentation and facilitate inspection for innacurate or inconsistent requirements. However, there exists a lack of tooling support for tabular expressions - this served as the primary motivation behind Tabster.
A Sample Application
Suppose we would like to design a triangle categorization system based on the side lengths of a given triangle inputted into our system as integers: a, b and c. A tabular expression representing these requirements is illustrated below - read the table from left to right to see how conditions are neatly compounded with each other to represent our requirements.
One of the main motivations for using tabular expressions was to check the completeness and consistency of complex specifications. Completeness ensures your system has considered the entire range of possible input into the system and consistency or disjointness ensures your specifications are deterministic - a single result exists for any given input. The Junit test below consumes Tabster’s api to verify completeness of our developed tabular expression thus far.
One important aspect of mission critical/embedded systems that is often overlooked involves considering boundary and out of range values. Tabster believes our expressions is incomplete because the system accepts integer values; however, we have not specified what the system should output when negative/zero values are entered. Furthermore, Tabster has provided us with the counter example [a = 0, b = 1, c = 2] to demonstrate exactly how our system currently lacks completeness. Lets go ahead and fix up our tabular expression. Notice the additional of an additional condition specifying what the system should output when an invalid side length is found.
And the modified Junit test is reproduced below.
Our tabular expression is now complete. For more information on interacting with the api or checking disjointness of tabular expressions, head over to Tabster’s GitHub page.
If you enjoyed this post, subscribe to my mailing list to be notified of future posts, and kindly share on Twitter .
