Specification and verification of fault-tolerance, timing, and scheduling

ABSTRACT

Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This article shows how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be usedto combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 2: Martín Abadi , Leslie Lamport, An Old-Fashioned Recipe for Real Time, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.1-27, June 03-07, 1991
• 3: ALPERN, B. AND SCHNEIDER, F. 1985. Defining liveness. Information Processing Letters 21, 4, 181-185.
• 4: ALUR, A., COURCOUBETIS, C., AND DILL, D. 1990. Model-checking for real-time systems. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Philadelphia, USA, 414-425.
• 5: ALUR, t. AND HENZINGER, T. 1990. Real-time logics: complexity and expressiveness. In Proceedings of the 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society, Philadelphia, USA, 390-401.
• 6: Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
• 7: AUDSLEY, N., BURNS, A., RICHARDSON, M., TINDELL, I{., AND WELLINGS, A. 1992. Applying new scheduling theory to static priority pre-emptive scheduling. Tech. Rep. RTRG/92/120, Department of Computer Science, University of York.
• 8: AVIZIENIS, A. 1976. Fault-tolerant systems. IEEE Transactions on Software Engineering C-25, 12 (December), 1304-1312.
• 9: R. J. R. Back, A calculus of refinements for program derivations, Acta Informatica, v.25 n.6, p.593-624, Aug. 1988 [doi>10.1007/BF00291051]
• 10: Nikolaj Bjørner , Zohar Manna , Henny Sipma , Tomás E. Uribe, Deductive Verification of Real-Time Systems Using STeP, Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software: Transformation-Based Reactive Systems Development, p.22-43, May 21-23, 1997
• 11: Marius Bozga , Conrado Daws , Oded Maler , Alfredo Olivero , Stavros Tripakis , Sergio Yovine, Kronos: A Model-Checking Tool for Real-Time Systems, Proceedings of the 10th International Conference on Computer Aided Verification, p.546-550, June 28-July 02, 1998
• 12: BURCH, J., CLARKE, E., DILL, D., HWANG, L., AND MCMILLAN, I{. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Philadelphia, USA, 428-439.
• 13: BURNS, t., DAVIS, R., AND PUNNEKKAT, S. 1995. Feasibility analysis of fault-tolerant real-time tasks. Tech. rep., Department of Computer Science, University of York.
• 14: BURNS, A. AND WELLINGS, A. 1996. Advanced fixed priority scheduling. In Real-Time Systems: Specification, Verification and Analysis, M. Joseph, Ed. Prentice Hall, London, 32-65.
• 15: Sérgio Vale Aguiar Campos , Edmund M. Clarke, The Versus Language: Representing Time Efficiently with BDDs, Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software: Transformation-Based Reactive Systems Development, p.64-78, May 21-23, 1997
• 16: CAMPOS, S., CLARKE, E., MARRERO, W., MINEA, M., AND HIRAISHI, H. 1994. Computing quantitative characteristics of finite-state real-time systems. In Proceedings of IEEE Real-time Systems Symposium. IEEE Computer Society Press, San Juan, Puerto Rico, USA.
• 17: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 18: E. M. Clarke , I. A. Browne , R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of &ohgr;-automata, Proceedings of the fifteenth colloquium on CAAP'90, p.103-116, May 1990, Copenhagen, Denmark
• 19: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 20: COENEN, J. AND HOOMAN, J. 1993. Parameterized semantics for fault-tolerant real-time systems. In Formal Techniques in Real-Time and Fault Tolerant Systems, J. Vytopil, Ed. Kluwer Academic Publishers, Boston, 51-78.
• 21: CRISTIAN, F. 1985. A rigorous approach to fault-tolerant programming. IEEE Transactions on Software Engineering SE-11, 1, 23-31.
• 22: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 23: Urban Engberg , Peter Grønning , Leslie Lamport, Mechanical Verification of Concurrent Systems with TLA, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.44-55, June 29-July 01, 1992
• 24: FIDGE, C. AND WELLINGS, t. 1997. An action-based formal model for concurrent, real-time systems. Formal Aspects of Computing 9, 2, 175-207.
• 25: Limor Fix , Fred B. Schneider, Reasoning About Programs by Exploiting the Environment, Cornell University, Ithaca, NY, 1994
• 26: Tom Henzinger , Zohar Manna , Amir Pnueli, Temporal proof methodologies for real-time systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.353-366, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99629]
• 27: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, Temporal proof methodologies for timed transition systems, Information and Computation, v.112 n.2, p.273-337, Aug 1 1994 [doi>10.1006/inco.1994.1060]
• 28: HENZINGER, T., NICOLLIN, X., SIFAKIS, J., AND YOVINE, S. 1992. Symbolic model checking for real-time systems. In Proceedings of the 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society, Santa Cruz, CA, USA.
• 29: J. Hooman, Specification and Compositional Verification of Real-Time Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1991
• 30: Tomasz Jankowski , Mathai Joseph, Dynamic Scheduling in the Presence of Faults: Specification and Verification, Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.279-297, September 09-13, 1996
• 31: JOSEPH, M. AND GOSWAMI, t. 1988. What's 'real' about real-time systems? In Proceedings of IEEE Real-time Systems Symposium. IEEE Computer Society Press, Huntsville, Alabama, 78-85.
• 32: JOSEPH, iV{. AND PANDYA, P. 1986. Finding response times in a real-time system. Computer Journal 29, 5, 390-395.
• 33: Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
• 34: KOYMANS, R. 1989. Specifying message passing and time-critical systems with temporal logic. Ph.D. thesis, Eindhoven University of Technology.
• 35: LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3, 2, 125-143.
• 36: LAMPORT, L. 1983. What good is temporal logic. In Proceedings of IFIP 9th World Congress, R. Mason, Ed. North-Holland, Amsterdam, the Netherlands, 657-668.
• 37: LAMPORT, L. 1985. Basic concepts. In Distributed Systems - Methods and Tools for Specification, Lecture Notes in Computer Science 190, M. Paul and H. Siegert, Eds. Springer-Verlag, Berlin.
• 38: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 39: Leslie Lamport , Stephan Merz, Specifying and Verifying Fault-Tolerant Systems, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.41-76, September 19-23, 1994
• 40: Leslie Lamport , Robert Shostak , Marshall Pease, The Byzantine Generals Problem, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.382-401, July 1982 [doi>10.1145/357172.357176]
• 41: LEHOCZKY, J., SHA, L., AND DING, Y. 1989. The rate-monotonic scheduling algorithms: exact characterisation and average case behaviour. In Proceedings of the 10th IEEE Real-time Systems Symposium. IEEE Computer Society Press, Santa Monica, CA, USA, 261-270.
• 42: C. L. Liu , James W. Layland, Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment, Journal of the ACM (JACM), v.20 n.1, p.46-61, Jan. 1973 [doi>10.1145/321738.321743]
• 43: Zhiming Liu, Fault-tolerant programming by transformations, University of Warwick, Coventry, UK, 1992
• 44: LIU, Z. AND JOSEPH, M. 1992. Transformation of programs for fault-tolerance. Formal Aspects of Computing ~, 5, 442-469.
• 45: LIU, Z. AND JOSEPH, M. 1993. Specifying and verifying recovery in asynchronous communicating systems. In Formal Techniques in Real-Time and Fault Tolerant Systems, J. Vytopil, Ed. Kluwer Academic Publishers, Boston, 137-166.
• 46: Zhiming Liu , Mathai Joseph, Stepwise Development of Fault-Tolerant Reactive Systems, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.529-546, September 19-23, 1994
• 47: Zhiming Liu , M. Joseph, Verification of fault tolerance and real time, Proceedings of the The Twenty-Sixth Annual International Symposium on Fault-Tolerant Computing (FTCS '96), p.220, June 25-27, 1996
• 48: LIu, Z. AND JOSEPH, M. 1996b. Verification of fault-tolerance and real-time. Tech. Rep. 1996/4, Department of Mathematics and Computer Science, University of Leicester.
• 49: Zhiming Liu , Mathai Joseph, Formalizing Real-Time Scheduling as Program Refinement, Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software: Transformation-Based Reactive Systems Development, p.295-309, May 21-23, 1997
• 50: Zhiming Liu , M. Joseph , Tomasz Janowski, Specifying Schedulability for Real-Time Programs, University of Warwick, Coventry, UK, 1993
• 51: LIU, Z., JOSEPH, M., AND JANOWSKI, T. 1995. Verification of schedulability of real-time programs. Formal Aspects of Computing 7, 5, 510-532.
• 52: Zhiming Liu , Anders P. Ravn , Xiaoshan Li, Verifying duration properties of timed transition systems, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.327-345, June 08-12, 1998
• 53: LOWE, G. AND ZEDAN, H. 1995. Refinement of complex systems: A case study. Tech. Rep. PRG- TR-2-95, Oxford University Computing Laboratory.
• 54: MANNA, Z. AND PNUELI, A. 1981. The temporal framework for concurrent programs. In The Correctness Problem in Computer Science, R. Boyer and J. Moore, Eds. Academic Press, Boston, 215-274.
• 55: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 56: Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992
• 57: MOITRA, A. AND JOSEPH, M. 1983. Cooperative recovery from faults in distributed programs. In Proceedings of IFIP 9th World Congress, R. Mason, Ed. North-Holland, Amsterdam, the Netherlands, 481-486.
• 58: NEUMANN, J. 1956. Probabilistic logics and the synthesis of reliable organisms from unreliable components. In In Automata Studies, C. E. Shannon and J. Macarthy, Eds. Princeton University Press, Princeton, 43-98.
• 59: Paritosh K. Pandya , H.-P. Wang , Qiwen Xu, Toward a theory of sequential hybrid programs, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.366-384, June 08-12, 1998
• 60: PNUELI, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, U.S.A, 46-57.
• 61: A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• 62: Amir Pnueli , Eyal Harel, Applications of temporal logic to the specification of real time systems (extended abstract), Proceedings of a Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.84-98, September 1988, Warwick, United Kingdom
• 63: Z. Qiu , C. Zhou, A combination of interval logic and linear temporal logic, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.444-461, June 08-12, 1998
• 64: RANDELL, B. 1975. System structure for software fault tolerance. IEEE Transactions on Software Engineering SE-1, 2 (June), 220-232.
• 65: B. Randell , P. Lee , P. C. Treleaven, Reliability Issues in Computing System Design, ACM Computing Surveys (CSUR), v.10 n.2, p.123-165, June 1978 [doi>10.1145/356725.356729]
• 66: SCHEPERS, H. AND GERTH, R. 1993. A compositional proof theory for fault-tolerant reM-time systerns. In Proceedings of the 12th Symposium on Reliable Distributed Systems. IEEE Computer Society Press, Princeton, N J, 34-43.
• 67: Richard D. Schlichting , Fred B. Schneider, Fail-stop processors: an approach to designing fault-tolerant computing systems, ACM Transactions on Computer Systems (TOCS), v.1 n.3, p.222-238, August 1983 [doi>10.1145/357369.357371]
• 68: Zheng Yuhua , Chaochen Zhou, A Formal Proof of the Deadline Driven Scheduler, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.756-775, September 19-23, 1994
• 69: Zhou Chaochen , Michael R. Hansen , Anders P. Ravn , Hans Rischel, Duration Specifications for Shared Processors, Proceedings of the Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.21-32, January 08-10, 1992
• 70: ZHOU, C., HOARE, C., AND RAVN, A. 1991. A calculus of durations. Information Processing Letters 40, 5 (December), 269-276.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Scheduling
      D.4.5 Reliability
          Subjects: Fault-tolerance
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory, Verification

Keywords:
fault-tolerance, real time, schedulability, specification, transformation, verification