This Article 
 Bibliographic References 
 Add to: 
Detecting Unsafe Error Recovery Schedules
August 1992 (vol. 18 no. 8)
pp. 749-760

A mechanism for modeling timing, precedence, and data-consistency constraints on concurrently executing processes is presented. The model allows durations and intervals between events to be specified. An algorithm is provided to detect schedules which may be unsafe with respect to the constraints. This work, motivated by the design and validation of autonomous error-recovery strategies on the Galileo spacecraft, appears to be applicable to a variety of asynchronous real-time systems.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] R. Alur and D. Dill, "Automata for modeling real-time systems," in17th ICALP, Lecture Notes in Computer Science, vol. 443. New York: Springer-Verlag, 1990, pp. 322-335.
[3] M. Ben-Ari,Principles of concurrent Programming. Englewood Cliffs, NJ: Prentice-Hall, 1982.
[4] A. J. Bernstein, "Analysis of programs for parallel processing,"IEEE Trans. Computers, vol. EC-15, pp. 757-762, Oct. 1966.
[5] A. A. Bestavros, J. J. Clark, and N. J. Ferrier, "Management of sensorimotor activity in mobile robots," inProc. 1990 IEEE Int. Conf. Robotics and Automation, pp. 592-597, 1990.
[6] G. Beutelschies,Galileo Space Flight Operations Plan, Command Dictionary. Pasadena, CA: Jet Propulsion Laboratory internal document, 625-505, vol. 11, Rev. A., 1989.
[7] R. H. Campbell and B. Randell, "Error recovery in asynchronous systems,"IEEE Trans. Software Eng., vol. SE-12, pp. 811-826, Aug. 1986.
[8] S. Cheng, J. A. Stankovic, and K. Ramamritham, "Dynamic scheduling of groups of tasks with precedence constraints in distributed hard real-time systems," inProc. IEEE Real-Time System Symp., pp. 166-174, 1986.
[9] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[10] J. E. Coolahan, Jr., and N. Roussopoulos, "A timed Petri net methodology for specifying real-time system timing requirements,"Int. Workshop on Timed Petri Nets, 1985.
[11] L. K. Dillonet al., "An interval logic based on actions and events," inProc. Berkeley Workshop on Temporal and Real-Time Specification, P.B. Ladkin and F.H. Vogt, Eds. Berkeley, CA: International Computer Science Institute, TR-90-060, pp. 33-45.
[12] E. A. Emerson, "Temporal and modal logic," inHandbook of Theoretical Computer Science, vol. B, Formal Models and Semantics., J. van Leeuwen, Ed. Cambridge/Amsterdam: MIT Press/Elsevier, 1990, pp. 995-1072.
[13] R. Backhouse, P. Chisholm, G. Malcolm, and E. Saaman, "Do-it-yourself type theory,"Formal Aspects Computing, vol. 1, pp. 19- 84, 1989.
[14] R. M. Fujimoto, "Parallel discrete event simulation,"Commun. ACM, vol. 33, no. 10, pp. 30-53, Oct. 1990.
[15] H. Garcia-Molina, "Using semantic knowledge for transaction processing in a distributed database,"ACM Trans. Database Syst., vol. 8, no. 2, June 1983.
[16] L. Grove,Galileo Space Flight Operations Plan, Fault Protection System Design and Operations. Pasadena, CA: Jet Propulsion Laboratory internal document, 625-505, vol. 8, Rev. A, Preliminary Release, Apr. 1989.
[17] 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.
[18] J. C. Horvath and L. P. Perry, "Hypercubes for critical spacecraft command verification,"AIAA Second Int. Symp. Space Information Systems, 1990.
[19] 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.
[20] W. H. Kohler, "A survey of techniques for synchronization and recovery in decentralized computer systems,"ACM Computing Surveys, vol. 13, pp. 149-182, June 1981.
[21] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE-13, no. 3, pp. 386-397, Mar. 1987.
[22] R. R. Lutz and J. S. K. Wong, "Validating system-level error recovery for spacecraft,"AIAA Computing in Aerospace 8, vol. 1, pp. 69-76, 1991.
[23] N. Lynch and H. Attiya, "Using mappings to prove timing properties,"MIT/LCS/TM-412.b, Dec. 1989.
[24] M. Maekawa, A. E. Oldehoeft, and R. R. Oldehoeft,Operating Systems: Advanced Concepts. Menlo Park, CA: Benjamin/Cummings, 1987.
[25] M. A. McDonald, "Functional emulation of engineering subsystem interactions within the Galileo spacecraft," M.S. thesis, Univ. Southern California, 1990.
[26] N. Medici,Galileo Spacecraft Flight Rules and Constraints. Pasadena, CA: Jet Propulsion Laboratory internal document, 625-270, Rev. C., July 1988.
[27] K. Mehlhorn,Graph Algorithms and NP-Completeness. New York: Springer-Verlag, 1984.
[28] J. E. B. Moss,Nested Transactions, An Approach to Reliable Distributed Computing. Cambridge, MA: MIT Press, 1981.
[29] J. D. Northcutt,Mechanisms for Reliable Distributed Real-Time Operating Systems, The Alpha Kernel. Boston: Academic Press, 1987.
[30] A. Pnueli and E. Harel, "Applications of temporal logic to the specifications of real time systems," inFormal Techniques in Real-Time and Fault-Tolerant Systems, M. Joseph, Ed. Berlin: Springer-Verlag, 1988, pp. 84-98.
[31] B. Randell, P.A. Lee, and P.C. Treleaven, "Reliability Issues in Computer System Design,"ACM Computing Surveys, Vol. 28, No. 2, Apr. 1978, pp. 123-165.
[32] R. R. Razouk and M. M. Gorlik, "A real time interval logic for reasoning about executions of real-time programs," inProc. ACM-SIGSOFT Conf., 1989.
[33] Relay/JOI Sequence, GLL3-120, Rev. D. Pasadena, CA: Jet Propulsion Laboratory internal document, pp. 108-177.
[34] R. L. Schwartz, P. M. Melliar-Smith, and F. H. Vogt, "An interval-based temporal logic,"Logics of Programs, Workshop, E. Clarke and D. Kozen, Eds.,Lecture Notes in Computer Science, vol. 164. Berlin: Springer-Verlag, 1984, pp. 443-457.
[35] L. Sha, R. Rajkumar, and J. P. Lehoczky, "Concurrency control for distributed real-time databases,"SIGMOD RECORD, vol. 17, pp. 82-98, Mar. 1988.
[36] J.A. Stankovic and K. Ramamritham,Hard Real-Time Systems, CS Press, Los Alamitos, Calif., 1984.
[37] D. J. Taylor, "How big can an atomic action be?" inProc. Fifth Symp. Reliability in Distributed Software and Database Systems, 1986, pp. 121-124.
[38] F. H. Vogt and S. Leue, "The paradigm of real-time specification based on interval logic," inProc. Berkeley Workshop on Temporal and Real-Time Specification, P. B. Ladkin and F. H. Vogt, Eds. Berkeley, CA: International Computer Science Institute TR-90-060, pp. 153-178.
[39] J. M. Wing, "A specifier's introduction to formal methods,"Computer, vol. 23, pp. 8-26, Sept. 1990.
[40] J. Xu and D. L. Parnas, "Scheduling processes with release times, deadlines, precedence, and exclusion relations,"IEEE Trans. Software Eng., vol. 16, pp. 360-369, Mar. 1990.

Index Terms:
unsafe error recovery schedules; modeling timing; precedence; data-consistency constraints; concurrently executing processes; Galileo spacecraft; asynchronous real-time systems; aerospace computing; fault tolerant computing; real-time systems; scheduling
R.R. Lutz, J.S.K. Wong, "Detecting Unsafe Error Recovery Schedules," IEEE Transactions on Software Engineering, vol. 18, no. 8, pp. 749-760, Aug. 1992, doi:10.1109/32.153384
Usage of this product signifies your acceptance of the Terms of Use.