Early safety analysis: From use cases to component-based software development

We propose an easy-to-use but formal approach for early safety analysis in the context of component-based software development and illustrate its application with a case example. Our approach aims at adopting formal safety analysis while maintaining flexibility and consistency throughout the development process. To this end, we use semi-formal use cases with templates that can be systematically translated into the formal specification language RSML^-e, whose execution environment integrates automated verification tools such as the model checker NuSMV. Consistency between use cases and the high-level component design is maintained through a systematic transition, so that the result of the safety analysis can be easily reflected in the design model.