The Modal Transition Analyser (MTSA) supports behaviour modelling, analysis and synthesis of concurrent software systems. Behaviour models are described using the Finite State Processes (FSP) language and behaviour constraints.