System modeling is the initial, and often crucial, step in verification. The right choice of model and modeling language is important for both designers and users of verification tools. This chapter aims to provide a guide to system modeling in four stages. First, it provides an overview of the main issues one must consider in modeling systems for verification. These issues involve both the selection or design of a modeling language and the steps of model creation. Next, it introduces a simple modeling language, sml, for illustrating the issues involved in selecting or designing a modeling language. sml uses an abstract state machine formalism that captures key features of widely-used languages based on transition system representations. We introduce the simple modeling language to simplify the connection between languages used by practitioners (such as Verilog, Simulink, or C) and various underlying formalisms (e.g., automata or Kripke structures) used in model checking. Third, the chapter demonstrates key steps in model creation using sml with illustrative examples. Finally, the presented modeling language sml is mapped to standard formalisms such as Kripke structures.