The aim of this paper is to describe a basic idea to introduce formal modelling in the development and presentation of e-learning systems. By introducing formalism, reasoning on e-learning systems and processes through them can be more easily understood. In particular, we propose to use Harel’s automata (statecharts) in modelling sequencing and navigation through learning …