You know, the embedded systems community has a heck of a lot of tools and formal logics for designing this stuff in the abstract. Lots of little DSLs and auto-checkers for thinking about processes and messages, that sort of thing. I'm not so sure about model -> code generation, I think that is mostly rolled by-hand.

For concurrency in the large, I wonder if there will be greater adoption of these sorts of engineering techniques.