This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Case-Study in Timed Refinement: A Mine Pump
September 1992 (vol. 18 no. 9)
pp. 817-826

A specification and top-level refinement of a simple mine pump control system, as well as a proof of correctness of the refinement, are presented as an example of the application of a formal method for the development of time-based systems. The overall approach makes use of a refinement calculus for timed systems, similar to the refinement calculi for sequential programs. The specification makes use of topologically continuous functions of time to describe both analog and discrete properties of both the system and its refinements. The basic building block of specifications is a specification statement that gives a clear separation between the specification of the assumptions that the system may make about the environment in which it is to be placed, and the effect the system is guaranteed to achieve if placed in such an environment. The top-level refinement of the system is developed by application of refinement laws that allow design decisions to be made, local state to be introduced, and the decomposition of systems into pipelined and/or parallel processes.

[1] R. J. R. Back, "A calculus of program derivations,"Acta Informatica, vol. 25, pp. 593-624, 1988.
[2] A. Burns and A. M. Lister, "A framework for building dependable systems,"The Computer Journal, vol. 34, pp. 173-182, Apr. 1991.
[3] A. Burns and A. Wellings, "Real-time systems and their programming languages," ch. 16,A Case Study in Ada. Reading, MA: Addison-Wesley, pp. 497-528, 1990.
[4] Z. Chaochen, C. A. R. Hoare, and A. P. Ravn, "A calculus of durations,"Tech. Rep. ProCoS Rep. OU ZCC2, Programming Research Group, Oxford University, 1991.
[5] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[6] I. J. Hayes, "A generalisation of bags in Z," in J. E. Nicholls, Ed.,Proc. Z User Meeting, Workshops in Computing, pp. 113-127, Dec. 1989.
[7] T. A. Henziger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for real-time systems," inProc. 18th ACM Symp. Principles of Programming Languages, pp. 353-366, 1991.
[8] G. E. Hughes and M. J. Cresswell,An Introduction to Modal Logic. Methuen, 1968.
[9] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[10] B. P. Mahony, "The specification and refinement of timed processes," Ph.D. dissertation, Univ. Queensland, 1992.
[11] B. P. Mahony and I. J. Hayes, "A case-study in timed refinement: A central heater," in J. M. Morris and R. C. Shaw, Eds.,Proc. 4th Refinement Workshop, pp. 138-149, 1991.
[12] B. P. Mahony and I. J. Hayes, "Using continuous real functions to model timed histories," inProc. 6th Australian Software Engineering Conf. (ASWEC91), 1991.
[13] C. C. Morgan, K. A. Robinson, and P. Gardiner, "On the refinement calculus,"Tech. Monograph PRG-70, Oxford University Programming Research Laboratory, 1988.
[14] C. C. Morgan, "The specification statement,"ACM Trans. Prog. Lang. and Syst., vol. 10, July 1988.
[15] J. M. Morris, "A theoretical basis for stepwise refinement and the programming calculus,"Science of Computer Programming, vol. 9, pp. 287-306, 1987.
[16] G. M. Reed, "A uniform theory for real-time distributed computing," Ph.D. dissertation, St. Edmund Hall, Oxford University, 1988.
[17] S. K. Shrivastava, L. V. Mancini, and B. Randell, "On the duality of fault tolerant system structures," inExperiences with Distributed Systems, vol. 309 ofLecture Notes in Computer Science, pp. 19-37, 1987.
[18] Sloman, M., and J. Kramer,Distributed Systems and Computer Networks, Prentice Hall, Englewood Cliffs, N.J., 1987.
[19] J. M. Spivey,The Z Notation: A Reference Manual (Computer Science Series). Englewood Cliffs, NJ: Prentice Hall International, 1989.
[20] C. Stirling, "An introduction to modal and temporal logics for CCS," in A. Yonezawa and T. Ito, Eds.,Concurrency: Theory, Language, and Architecture, LNCS 491, pp. 2-20, 1991.

Index Terms:
top-level refinement; simple mine pump control system; proof of correctness; formal method; time-based systems; refinement calculus; timed systems; sequential programs; topologically continuous functions; discrete properties; basic building block; specification statement; refinement laws; design decisions; pipelined; parallel processes; computerized monitoring; formal specification; mining; pumps; theorem proving
Citation:
B.P. Mahony, I.J. Hayes, "A Case-Study in Timed Refinement: A Mine Pump," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 817-826, Sept. 1992, doi:10.1109/32.159841
Usage of this product signifies your acceptance of the Terms of Use.