In this paper the author uses Alloy, as a modeling lan- guage, 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 in- stances of the model are generated without making a line of code. The paper presents two models based on the for- mal 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.