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

Date
1999
Authors
Chen, Zhiqiang
Cau, A. (Antonio)
Zedan, Hussein
Yang, Hongji
Journal Title
Journal ISSN
ISSN
Volume Title
Publisher
Elsevier
Peer reviewed
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.
Description
Keywords
object-oriented, refinement calculus, temporal agent model, semantics, EPSRC GR/M/02583
Citation
Chen, Zhiqiang et al. (1999) Integrating structured OO approaches with formal techniques for the development of real-time systems. Information and Software Technology, 41 (7), pp. 435-450
Research Institute