A practitioner’s handbook (HB) about the application of Formal Methods of computing to a particular domain —in our case: the railway domain [9]— must bridge the gap between Formal Methods (which are closely related to theoretical computer science), as such, and their practical applicability by those engineers who have perhaps never studied theoretical computer science in all its scholarly details.