Abstract. This chapter is a short introduction to the Event-B modelling method for discrete transition systems. Important mechanisms for the step-wise development of the formal models, such as context extension and machine refinement, are dis- cussed. Consistency of the models are presented in terms of proof obligations and are illustrated by concrete examples.