Using spreadsheets for finite state modelling

ABSTRACT

State based modelling is a widely used practice in the software industry. There are two methods of building state based models: either using graphical modelling tools, or using formal languages like SMV or SAL. The former method often suffers from the problem of cost, in particular, when the modelling requirements are lightweight, purchase of an elaborate modelling tool does not turn out to be cost effective. The latter method suffers from learning complexity problem. Software engineers, who write the specifications, are usually not familiar with formal languages On the other hand, a large number of software engineers find it convenient to write their specifications semi-formally using tools such as spreadsheets. We formalise the spreadsheet finite modelling language and demonstrate that it is expressive enough to capture most important notions of finite state modelling. We show that this language is sufficiently usable in terms of readability and maintainability. We also present SAL-gen, a tool that takes as an input a finite state model written in our language, and generates corresponding SAL code. This can form the basis for analysis tools such as property checkers and test generators using the existing SAL tool set.

REFERENCES

• 1: Leonardo de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, and Ashish Tiwari. Sal 2. In CAV, pages 496--500, 2004.
• 2: Leonardo de Moura Gregoire Hamon and John Rushby. Automated Test Generation using SAL. Technical report, SRI International, 2005.
• 3: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 4: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 5: H. Hong, I. Lee, O. Sokolsky, and S. Cha. Automatic Test Generation from Statecharts using Model Checking, 2001.
• 6: John E. Hopcroft , Rajeev Motwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 7: IEEE. IEEE Standard Glossary of Software Engineering Terminology.
• 8: Nancy A. Lynch , Frits W. Vaandrager, Forward and Backward Simulations for Timing-Based Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.397-446, June 03-07, 1991
• 9: Mathworks. Stateflow 7.0.
• 10: Srikanth Mujjiga and Srihari Sukumaran. Generating Tests for Validating Devices for CEC Compliance. Technical report, Philips Research, 2007.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Algorithms, Languages

Keywords:
finite state machines, sal, spreadsheets