Abstract
An object based formal method for the development of real-time systems, called ATOM, is presented. The method is an integration of the real-time formal technique TAM (Temporal Agent Model) with an industry-strength structured methodology known as HRT-HOOD. ATOM is a systematic formal approach based on the refinement calculus. Within ATOM, a formal specification (or abstract description statement) contains Interval Temporal Logic (ITL) description of the timing, functional, and communication behavior of the proposed real-time system. This formal specification can be analyzed and then refined into concrete statements through successive applications of sound refinement laws. Both abstract and concrete statements are allowed to freely intermix. The semantics of the concrete statements in ATOM are defined denotationally in specification-oriented style using ITL.
Similar content being viewed by others
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Zedan, H., Cau, A., Chen, Z. et al. ATOM: An object-based formal method for real-time systems. Annals of Software Engineering 7, 235–256 (1999). https://doi.org/10.1023/A:1018942406449
Issue Date:
DOI: https://doi.org/10.1023/A:1018942406449