Describing Platooning in the language of MWB (Mobility Workbench), a tool for manipulating and analyzing mobile concurrent systems described in pi-calculus (tool written in standard SML and runs on SML/NJ compiler). Then describing it in Promela to model check using SPIN and Isabelle