Special:Publication/jastram forms 2012
Formal methods are experiencing a renaissance, especially in the development of safety-critical systems. An indicator for this is the fact that more and more standards either recommend or prescribe the use of formal methods.
Using formal methods on an industrial scale requires their integration into the system engineering process. This paper is exploring how an integrated tool chain that supports formal methods may look like. It thereby focusses on our experience with tool chains that are based on the open source Eclipse platform in general, and the Rodin formal modeling environment in particular.
Open Source allows organisations to remedy the risk of being dependent on one single vendor. This includes the risk of the feature set provided: users can add missing features themselves or commission their inclusion to any competent party, rather than having to rely on the vendor to implement it. It further includes the risk of maintenance and long-term support.
We see industrial interest in open source for systems engineering in general, and Eclipse in particular. Eclipse is attractive, because its license is business-friendly. Further, its modular architecture makes it easy to seamlessly integrate the various Eclipse-based tools for systems engineering.
This paper focuses on an ecosystem that is accumulated around two Eclipse-based platforms, First, the Rodin platform is an open source modeling environment for the Event-B formalism. Second, the Requirements Modeling Framework (RMF) is a platform for working with natural language requirements, supporting the international ReqIF standard.