Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm
In recent years, large sectors of the software development industry have moved from the procedural style of software development to an object-oriented style. Safety-critical software developers have largely resisted this trend because of concerns about verifiability of object-oriented systems. This paper outlines the benefits offered by object technology and considers the key features of the object-oriented approach from a user’s perspective. We review the main issues affecting safety and propose a paradigm — Verified Design-by-Contract — that uses formal methods to facilitate the safe use of inheritance, polymorphism, dynamic binding and other features of the object-oriented approach. An outline of Perfect Developer — a tool supporting the Verified Design-by-Contract paradigm — is included.
KeywordsUnify Modeling Language Verification Condition Object Technology Unify Modeling Language Model Dynamic Binding
Unable to display preview. Download preview PDF.
- Bames J (1997). High Integrity Ada: the SPARK Approach. Addison-Wesley, England.Google Scholar
- Chalin P (2003). Improving JML: For a Safer and More Effective Language. FME 2003: Formal Methods (Springer LNCS 2805): 440.Google Scholar
- Kramer R (1998). iContract - The Java(tm) Design by Contract(tm) Tool. Technology of Object-Oriented Languages and Systems, August 03–07: 295.Google Scholar
- Meyer B (1988). Object-Oriented Software Construction. Prentice Hall, England.Google Scholar
- OOTiA (2003). Handbook for Object-Oriented Technology in Aviation (draft). OOTiA Workshop Proceedings, March 5, 2003.Google Scholar
- Port D and McArthur M (1999). A Study of Productivity and Efficiency for Object-Oriented Methods and Languages. APSEC 1999 (IEEE Computer Society): 128-.Google Scholar
- RTJ (2003). http://www.rtj.org (30 September 2003).Google Scholar
- Warren J.H and Oldman R.D (2003). A Rigorous Specification Technique for High Quality Software, Proceedings of the Twelfth Safety-Critical Systems Symposium, Springer-Verlag (London).Google Scholar