
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
B.P. Mahony, I.J. Hayes, "A CaseStudy in Timed Refinement: A Mine Pump," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 817826, September, 1992.  
BibTex  x  
@article{ 10.1109/32.159841, author = {B.P. Mahony and I.J. Hayes}, title = {A CaseStudy in Timed Refinement: A Mine Pump}, journal ={IEEE Transactions on Software Engineering}, volume = {18}, number = {9}, issn = {00985589}, year = {1992}, pages = {817826}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.159841}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A CaseStudy in Timed Refinement: A Mine Pump IS  9 SN  00985589 SP817 EP826 EPD  817826 A1  B.P. Mahony, A1  I.J. Hayes, PY  1992 KW  toplevel refinement; simple mine pump control system; proof of correctness; formal method; timebased 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 VL  18 JA  IEEE Transactions on Software Engineering ER   
A specification and toplevel 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 timebased 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 toplevel 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. 593624, 1988.
[2] A. Burns and A. M. Lister, "A framework for building dependable systems,"The Computer Journal, vol. 34, pp. 173182, Apr. 1991.
[3] A. Burns and A. Wellings, "Realtime systems and their programming languages," ch. 16,A Case Study in Ada. Reading, MA: AddisonWesley, pp. 497528, 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: PrenticeHall 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. 113127, Dec. 1989.
[7] T. A. Henziger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for realtime systems," inProc. 18th ACM Symp. Principles of Programming Languages, pp. 353366, 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 realtime systems,"IEEE Trans. Software Eng., vol. SE12, no. 9, pp. 890904, 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 casestudy in timed refinement: A central heater," in J. M. Morris and R. C. Shaw, Eds.,Proc. 4th Refinement Workshop, pp. 138149, 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 PRG70, 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. 287306, 1987.
[16] G. M. Reed, "A uniform theory for realtime 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. 1937, 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. 220, 1991.