Extending Eclipse to support object-oriented system verification

The software development is facing increasingly stringent demands with regard to complexity, reliability and safety, especially in the areas of consumer electronics and in automotive, military and aerospace technology as well as in telecommunications and data communications. The stronger emphasis placed on safety-critical systems is being driven by the fact that the military and aerospace technology areas are growing as fields of application in nearly all areas of software development. Formal methods have long held the promise of providing a much-needed solid engineering foundation for the ´art´ of programming computers. Formal specifications can be used to provide an unambiguous and precise supplement to natural language descriptions and can be rigorously validated and verified leading to the early detection of specification errors. This paper introduces an integrated formal framework for Eclipse platform in the development of software for safety critical systems to greatly improve the applicability of the Eclipse platform in these applications.