×

Transformational vs reactive refinement in real-time systems. (English) Zbl 0875.68145

Summary: Real-time software development is investigated in an extended form of the Z language, and compared with development in the Temporal Agent Model (TAM): a theory specifically designed for real-time systems. Both of these theories use refinement as the main development method, and by defining a translation between the extended Z language, and the TAM language, we are able to compare the two refinement relations in terms of an example real-time system refinement.

MSC:

68M99 Computer system organization
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Z
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Fidge, C., Real-time refinement, (Woodcock, J.; Larsen, P., FME’93: Industrial-Strength Formal Methods. FME’93: Industrial-Strength Formal Methods, Lecture Notes in Computer Science, 670 (1993), Springer: Springer Berlin) · Zbl 0830.68088
[2] Fidge, C., Adding real time to formal program development, (Tech. Rept. 94-12 (1994), SVRC, University of Queensland)
[3] Mahony, B. P.; Hayes, I. J., A case study in timed refinement: A mine pump, IEEE Trans. Software Engineering, 18, 817-825 (1992)
[4] Potter, B.; Sinclair, J.; Till, D., An Introduction to Formal Specification and Z (1991), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0745.68028
[5] Scholefield, D., TAM technical notes 1 and 2, (Tech. Rept. YCS213 (1993), University of York)
[6] Scholefield, D. J., The formal development of real-time systems: A review, (Tech. Rept. YCS145 (1990), University of York)
[7] Scholefield, D. J., A refinement calculus for real-time systems, (Ph.D. Thesis (1992), University of York)
[8] Scholefield, D. J.; Zedan, H. S.M., A standard for finite TAM, (Tech. Rept. YCS206 (1993), University of York) · Zbl 0769.68086
[9] Scholefield, D. J.; Zedan, H. S.M.; He, J., A specification oriented semantics for the refinement of real-time systems, Theoret. Comput. Sci., 131, 219-241 (1994) · Zbl 0820.68071
[10] Spivey, J., Understanding Z, (Cambridge Tracts in Theoretical Computer Science, 3 (1988), Cambridge University Press: Cambridge University Press Cambridge) · Zbl 1147.68567
[11] Spivey, J. M., (The Z notation — A reference Manual (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ) · Zbl 0777.68003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.