From Abstract Representation To Formal Modelling Of Tactical Military Operations