Integrating domain Specific language design in the software life cycle

Domain Specific Languages help to split the software live cycle in different independent cycles. While the use of the newly created language is just an additional tool in the established cycle, the language live cycle is independent and opens the doors for the application of formal methods. We report on an industrial case study, where a driver specification language has been designed, formally specified, and finally an implementation has been generated from the specification. Using Abstract State Machines and Montages for the language specification, it was possible that the industrial partners learned how to maintain and extend the language specification. On the other hand the formal semantics of the method allows to apply different verification-oriented methods to the artifacts.