Disciplined methods of software specification: a case study

We describe our experience applying tabular mathematical approaches to software specifications. Our purpose is to show alternative approaches to writing tabular specifications and to help practitioners who want to apply such methods by allowing them to pick the best one for their problem. The object for the case study is software used by Dell Products for testing the functionality of the keyboards on notebook computers. Starting from informal documents, we developed a variety of tabular representations of finite state machine specifications and tabular trace specifications. We found that the discipline required by these methods raised issues that had never been considered and resulted in documents that were both more complete and much clearer. The various tabular representations are compared from a user's point of view, i.e., clarity, consistency, unambiguity, completeness, suitability, etc.