A Formal Model for the Building of State Machines: A Lightweight Approach

In this paper the author uses Alloy, as a modeling language, to model the elements that form a state machine and the rules that govern how they can be connected. This modeling language is also a formal method that develops a model incrementally and can analyze it in an early state of the design having the advantage of detecting modeling errors very quickly. By using the formal method, some instances of the model are generated without making a line of code. The paper presents two models based on the formal approach: a graphical model and a textual model. The graphical model is used as an overview of the system and the textual model to establish further constraints on the graphical model.