Integrating structured OO approaches with formal techniques for the development of real-time systems

Abstract

The use of formal methods in the development of time-critical applications is essential if we want to achieve a high level of assurance in them. However, these methods have not yet been widely accepted in industry as compared to the more established structured and informal techniques. A reliable linkage between these two techniques will provide the developer with a powerful tool for developing a provably correct system. In this paper, we explore the issue of integrating a real-time formal technique, TAM (Temporal Agent Model), with an industry-strength structured methodology known as HRT-HOOD. TAM is a systematic formal approach for the development of real-time systems based on the refinement calculus. Within TAM, a formal specification can be written (in a logic-based formalism), analysed and then refined to concrete representation through successive applications of sound refinement laws. Both abstract specification and concrete implementation are allowed to freely intermix. HRT-HOOD is an extension to the Hierarchical Object-Oriented Design (HOOD) technique for the development of Hard Real-Time systems. It is a two-phase design technique dealing with the logical and physical architecture designs of the system which can handle both functional and non-functional requirement, respectively. The integrated technique is illustrated on a version of the mine control system.