In large part because those models are easy to formally verify. I've become interested in SPARK of the past few years, but people tell me while you can verify it, it is hard to do right. (I have no idea)
I don't work with them myself, but some of my coworkers do low level control of similar hardware and they mostly work in matlab for that reason. Well for new code, there is still a lot of C from 20+ years ago in production, it isn't formally verified but years of real world experience says it is pretty good. Everytime there is a new feature there is a decision to rewrite the whole in matlab, put in shims to write the new part in matlab, or just add the C.
