On 24 Feb 2007, at 09:06, Zoe Brain wrote:

> I'm doing my PhD on automotive software development. We already  
> have a nice model compiler that takes requirements (not designs)  
> expressed in xtUML and generates Ada-95 systems from them. Contact  
> http://www.softimp.com.au and ask about their BILBY model compiler.

My experience of xUML (actually its predecessor, and from a  
competitor at that) was that you ended up doing quite a lot of  
design, and even programming -- just not in Ada.

> We hope to apply that to automotive systems soon - measuring  
> footprint, real-time performance and so on. After that, re-jig the  
> model compiler so it produces SPARK-95, and code  that complies  
> with avionics standards and is also formally provable.

Presumably for any really interesting SPARK annotations you'd have to  
decorate the model? The model compiler can make deductions from the  
model but I would have expected them to be about modelling (eg  
multiplicities), not so much about automotive systems.