If you know good introductions to those tools, I'd be happy to look! Most of my experience is in things like PRISM, Alloy, TLA+, etc, and I don't have experience with those three. At least on a quick search, one difference between TLA+ and SCADE and Simulink is it's free and open source. mCRL2 is also free and open source, looks like, so that's probably the easiest for me to start looking at.