Using Spreadsheets for Finite State Modelling

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.