Executable analysis of MP behavior architectures is possible with the use of automated tools. NPS has a public implementation of MP called MP-Firebird:
https://firebird.nps.edu

MP-Firebird first became available to the public in June 2015. It has been used in NPS courses SE4003 Software Systems Engineering, SE4930 Model Based Systems Engineering, SE4935 Formal Methods for Systems Architecting, and SE3302 Systems Suitability. It has also been used in directed studies, thesis and doctoral research, and to support numerous sponsored research studies for ONR, NAVAIR, NAWC, MCSC, NRP and CRUSER.
NPS students, faculty and staff: Log in for access to pre-release software (left menu).