Advertisement

An Overview of Formal Verification for the Time-Triggered Architecture

  • John Rushby
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)

Abstract

We describe formal verification of some of the key algorithms in the Time-Triggered Architecture (TTA) for real-time safety-critical control applications. Some of these algorithms pose formidable challenges to current techniques and have been formally verified only in simplified form or under restricted fault assumptions. We describe what has been done and what remains to be done and indicate some directions that seem promising for the remaining cases and for increasing the automation that can be applied. We also describe the larger challenges posed by formal verification of the interaction of the constituent algorithms and of their emergent properties.

Keywords

Linear Temporal Logic Clock Synchronization Faulty Node Global Schedule Byzantine Fault 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Anish Arora and Sandeep S. Kulkarni. Detectors and correctors: A theory of fault-tolerance components. In 18th International Conference on Distributed Computing Systems, pages 436–443, Amsterdam, The Netherlands, 1998. IEEE Computer Society.Google Scholar
  2. 2.
    Günther Bauer and Michael Paulitsch. An investigation of membership and clique avoidance in TTP/C. In 19th Symposium on Reliable Distributed Systems, Nuremberg, Germany, October 2000.Google Scholar
  3. 3.
    Kai Baukus, Saddek Bensalem, Yassine Lakhnech, and Karsten Stahl. Abstracting WS1S systems to verify parameterized networks. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 188–203, Berlin, Germany, March 2000. Springer-Verlag.CrossRefGoogle Scholar
  4. 4.
    Kai Baukus, Yassine Lakhnech, and Karsten Stahl. Verifying universal properties of parameterized networks. In Matthai Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of Lecture Notes in Computer Science, pages 291–303, Pune, India, September 2000. Springer-Verlag.CrossRefGoogle Scholar
  5. 5.
    Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, and Yassine Lakhnech. A transformational approach for generating non-linear invariants. In Jens Palsberg, editor, Seventh International Static Analysis Symposium (SAS’00), volume 1824 of Lecture Notes in Computer Science, pages 58–74, Santa Barbara CA, June 2000. Springer-Verlag.Google Scholar
  6. 6.
    Saddek Bensalem and Yassine Lakhnech. Automatic generation of invariants. Formal Methods in Systems Design, 15(1):75–92, July 1999.Google Scholar
  7. 7.
    Ahmed Bouajjani and Agathe Merceron. Parametric verification of a group membership algorithm. These proceedings.Google Scholar
  8. 8.
    Tushar D. Chandra, Vassos Hadzilacos, Sam Toueg, and Bernadette Charron-Bost. On the impossibility of group membership. In Fifteenth ACM Symposium on Principles of Distributed Computing, pages 322–330, Philadelphia, PA, May 1996. Association for Computing Machinery.Google Scholar
  9. 9.
    James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439–448, Limerick, Ireland, June 2000. IEEE Computer Society.Google Scholar
  10. 10.
    S. J. Creese and A. W. Roscoe. TTP: A case study in combining induction and data independence. Technical Report PRG-TR-1-99, Oxford University Computing Laboratory, Oxford, England, 1999.Google Scholar
  11. 11.
    Ben L. Di Vito and Ricky W. Butler. Formal techniques for synchronized fault tolerant systems. In C. E. Landwehr, B. Randell, and L. Simoncini, editors, Dependable Computing for Critical Applications—3, volume 8 of Dependable Computing and Fault-Tolerant Systems, pages 163–188. Springer-Verlag, Vienna, Austria, September 1992.Google Scholar
  12. 12.
    Jacob Elgaard, Nils Klarlund, and Anders Möller. Mona 1.x: New techniques for WS1S and WS2S. In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, pages 516–520, Vancouver, Canada, June 1998. Springer-Verlag.CrossRefGoogle Scholar
  13. 13.
    E. A. Emerson and A. P. Sistla, editors. Computer-Aided Verification, CAV’ 2000, volume 1855 of Lecture Notes in Computer Science, Chicago, IL, July 2000. Springer-Verlag.Google Scholar
  14. 14.
    J.-C. Filliâtre, S. Owre, H. Rueβ, and N. Shankar. ICS: Integrated Canonization and Solving. In G. Berry, H. Comon, and A. Finkel, editors, Computer-Aided Verification, CAV’ 2001, volume 2102 of Lecture Notes in Computer Science, pages 246–249, Paris, France, July 2001. Springer-Verlag.Google Scholar
  15. 15.
    Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(2):374–382, April 1985.Google Scholar
  16. 16.
    N. Henderson and S. E. Paynter. The formal classification and verification of Simpson’s 4-slot asynchronous communication mechanism. In Peter Lindsay, editor, Formal Methods Europe (FME’02), Lecture Notes in Computer Science, Copenhagen, Denmark, July 2002. Springer-Verlag. To appear.Google Scholar
  17. 17.
    T.A. Henzinger, B. Horowitz, and C.M. Kirsch. Giotto: a time-triggered language for embedded programming. In Henzinger and Kirsch [18], pages 166–184.Google Scholar
  18. 18.
    Tom Henzinger and Christoph Kirsch, editors. EMSOFT 2001: Proceedings of the First Workshop on Embedded Software, volume 2211 of Lecture Notes in Computer Science, Lake Tahoe, CA, October 2001. Springer-Verlag.Google Scholar
  19. 19.
    C. B. Jones. Tentative steps toward a development method for interfering programs. A CM TOPLAS, 5(4):596–619, 1983.zbMATHCrossRefGoogle Scholar
  20. 20.
    Shmuel Katz, Pat Lincoln, and John Rushby. Low-overhead time-triggered group membership. In Marios Mavronicolas and Philippas Tsigas, editors, 11th International Workshop on Distributed Algorithms (WDAG’ 97), volume 1320 of Lecture Notes in Computer Science, pages 155–169, Saarbrücken Germany, September 1997. Springer-Verlag.Google Scholar
  21. 21.
    Herman Kopetz and R. Nossal. Temporal firewalls in large distributed real-time systems. In 6th IEEE Workshop on Future Trends in Distributed Computing, pages 310–315, Tunis, Tunisia, October 1997. IEEE Computer Society.Google Scholar
  22. 22.
    Hermann Kopetz. Real-Time Systems: Design Princples for Distributed Embedded Applications. The Kluwer International Series in Engineering and Computer Science. Kluwer, Dordrecht, The Netherlands, 1997.Google Scholar
  23. 23.
    Hermann Kopetz. The time-triggered model of computation. In Real Time Systems Symposium, Madrid, Spain, December 1998. IEEE Computer Society.Google Scholar
  24. 24.
    Hermann Kopetz. Elementary versus composite interfaces in distributed real-time systems. In The Fourth International Symposium on Autonomous Decentralized Systems, Tokyo, Japan, March 1999. IEEE Computer Society.Google Scholar
  25. 25.
    Hermann Kopetz and Günter Grünsteidl. TTP—a protocol for fault-tolerant real time systems. IEEE Computer, 27(1):14–23, January 1994.Google Scholar
  26. 26.
    Hermann Kopetz and Johannes Reisinger. The non-blocking write protocol NBW: A solution to a real-time synchronization problem. In Real Time Systems Symposium, pages 131–137, Raleigh-Durham, NC, December 1993. IEEE Computer Society.Google Scholar
  27. 27.
    Sandeep Kulkarni, John Rushby, and N. Shankar. A case study in component based mechanical verification of fault-tolerant programs. In ICDCS Workshop on S elf-Stabilizing Systems, pages 33–40, Austin, TX, June 1999. IEEE Computer Society.Google Scholar
  28. 28.
    Sandeep S. Kulkarni. Component-Based Design of Fault Tolerance. PhD thesis, The Ohio State University, Columbus, OH, 1999.Google Scholar
  29. 29.
    L. Lamport and P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1):52–78, January 1985.Google Scholar
  30. 30.
    Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine Generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382–401, July 1982.Google Scholar
  31. 31.
    Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Series in Data Management Systems. Morgan Kaufmann, San Francisco, CA, 1996.zbMATHGoogle Scholar
  32. 32.
    Keith Marzullo. Tolerating failures of continuo us-valued sensors. ACM Transactions on Computer Systems, 8(4):284–304, November 1990.Google Scholar
  33. 33.
    K. L. McMillan. Circular compositional reasoning about liveness. In Laurence Pierre and Thomas Kropf, editors, Advances in Hardware Design and Verification: IFIP WG10.5 International Conference on Correct Hardware Design and Verification Methods (CHARME’ 99), volume 1703 of Lecture Notes in Computer Science, pages 342–345, Bad Herrenalb, Germany, September 1999. Springer-Verlag.Google Scholar
  34. 34.
    Paul S. Miner. Verification of fault-tolerant clock synchronization systems. NASA Technical Paper 3349, NASA Langley Research Center, Hampton, VA, November 1993.Google Scholar
  35. 35.
    Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417–426, July 1981.Google Scholar
  36. 36.
    Kedar S. Namjoshi and Richard J. Trefler. On the completeness of compositional reasoning. In Emerson and Sistla [13], pages 139–153.CrossRefGoogle Scholar
  37. 37.
    Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.Google Scholar
  38. 38.
    Michael Paulitsch and Wilfried Steiner. The transition from asynchronous to synchronous system operation: An approach for distributed fault-tolerant systems. In The 22nd International Conference on Distributed Computing Systems (ICDCS 2002), Vienna, Austria, July 2002. IEEE Computer Society. To appear.Google Scholar
  39. 39.
    M. Pease, R. Shostak, and L. Lamport. Reaching agreement in the presence of faults. Journal of the ACM, 27(2):228–234, April 1980.Google Scholar
  40. 40.
    Holger Pfeifer. Formal verification of the TTA group membership algorithm. In Tommaso Bolognesi and Diego Latella, editors, Formal Description Techniques and Protocol Specification, Testing and Verification FORTE XIII/PSTV XX 2000, pages 3–18, Pisa, Italy, October 2000. Kluwer Academic Publishers.Google Scholar
  41. 41.
    Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke. Formal verification for time-triggered clock synchronization. In Weinstock and Rushby [72], pages 207–226.Google Scholar
  42. 42.
    Stefan Poledna. Fault-Tolerant Systems: The Problem of Replica Determinism. The Kluwer International Series in Engineering and Computer Science. Kluwer, Dordrecht, The Netherlands, 1996.zbMATHGoogle Scholar
  43. 43.
    John Rushby. The design and verification of secure systems. In Eighth ACM Symposium on Operating System Principles, pages 12–21, Asilomar, CA, December 1981. (ACM Operating Systems Review, Vol. 15, No. 5).Google Scholar
  44. 44.
    John Rushby. A fault-masking and transient-recovery model for digital flight-control systems. In Jan Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, Kluwer International Series in Engineering and Computer Science, chapter 5, pages 109–136. Kluwer, Boston, Dordecht, London, 1993.Google Scholar
  45. 45.
    John Rushby. A formally verified algorithm for clock synchronization under a hybrid fault model. In Thirteenth ACM Symposium on Principles of Distributed Computing, pages 304–313, Los Angeles, CA, August 1994. Association for Computing Machinery. Also available as NASA Contractor Report 198289.Google Scholar
  46. 46.
    John Rushby. Automated deduction and formal methods. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, pages 169–183, New Brunswick, NJ, July/August 1996. Springer-Verlag.Google Scholar
  47. 47.
    John Rushby. Partitioning for avionics architectures: Requirements, mechanisms, and assurance. NASA Contractor Report CR-1999-209347, NASA Langley Research Center, June 1999. Available at http://www.csl.sri.com/~rushby/abstracts/partition, and http://techreports.larc.nasa.gov/ltrs/PDF/1999/cr/NASA-99-cr209347.pdf; also issued by the FAA.
  48. 48.
    John Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering, 25(5):651–660, September/October 1999.Google Scholar
  49. 49.
    John Rushby. Verification diagrams revisited: Disjunctive invariants for easy verification. In Emerson and Sistla [13], pages 508–520.CrossRefGoogle Scholar
  50. 50.
    John Rushby. Bus architectures for safety-critical embedded systems. In Henzinger and Kirsch[18]. pages 306–323.Google Scholar
  51. 51.
    John Rushby. A comparison of bus architectures for safety-critical embedded systems. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, September 2001. Available at http://www.csl.sri.com/~rushby/abstracts/buscompare.Google Scholar
  52. 52.
    John Rushby. Formal verification of McMillan’s compositional assume-guarantee rule. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, September 2001.Google Scholar
  53. 53.
    John Rushby. Formal verification of transmission window timing for the time-triggered architecture. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, March 2001.Google Scholar
  54. 54.
    John Rushby. Formal verificaiton of Marzullo’s sensor fusion interval. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, January 2002.Google Scholar
  55. 55.
    John Rushby and Friedrich von Henke. Formal verification of algorithms for critical systems. IEEE Transactions on Software Engineering, 19(1):13–23, January 1993.Google Scholar
  56. 56.
    John Rushby, Friedrich von Henke, and Sam Owre. An introduction to formal specification and verification using Ehdm. Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1991.Google Scholar
  57. 57.
    Hassen Saÿdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer-Aided Verification, CAV’ 97, volume 1254 of Lecture Notes in Computer Science, pages 72–83, Haifa, Israel, June 1997. Springer-Verlag.Google Scholar
  58. 58.
    Hassen Saÿdi and N. Shankar. Abstract and model check while you prove. In Nicolas Halbwachs and Doron Peled, editors, Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, pages 443–454, Trento, Italy, July 1999. Springer-Verlag.CrossRefGoogle Scholar
  59. 59.
    Ulrich Schmid. How to model link failures: A perception-based fault model. In The International Conference on Dependable Systems and Networks, pages 57–66, Goteborg, Sweden, July 2001. IEEE Computer Society.Google Scholar
  60. 60.
    Ulrich Schmid and Klaus Schossmaier. How to reconcile fault-tolerant interval intersection with the Lipschitz condition. Distributed Computing, 14(2):101–111, May 2001.Google Scholar
  61. 61.
    Fred B. Schneider. Understanding protocols for Byzantine clock synchronization. Technical Report 87-859, Department of Computer Science, Cornell University, Ithaca, NY, August 1987.Google Scholar
  62. 62.
    Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299–319, December 1990.Google Scholar
  63. 63.
    Marco Schneider. Self stabilization. ACM Computing Surveys, 25(1):45–67, March 1993.Google Scholar
  64. 64.
    D. Schwier and F. von Henke. Mechanical verification of clock synchronization algorithms. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, pages 262–271, Lyngby, Denmark, September 1998. Springer-Verlag.CrossRefGoogle Scholar
  65. 65.
    Natarajan Shankar. Mechanical verification of a generalized protocol for Byzantine fault-tolerant clock synchronization. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 217–236, Nijmegen, The Netherlands, January 1992. Springer-Verlag.Google Scholar
  66. 66.
    Natarajan Shankar. Combining theorem proving and model checking through symbolic analysis. In CONCUR 2000: Concurrency Theory, number 1877 in Lecture Notes in Computer Science, pages 1–16, State College, PA, August 2000. Springer-Verlag. Available at ftp://ftp.csl.sri.com/pub/users/shankar/concur2000.ps.gz.CrossRefGoogle Scholar
  67. 67.
    H. R. Simpson. Four-slot fully asynchronous communication mechanism. IEE Proceedings, Part E: Computers and Digital Techniques, 137(1):17–30, January 1990.Google Scholar
  68. 68.
    T. K. Srikanth and Sam Toueg. Optimal clock synchronization. Journal of the ACM, 34(3):626–645, July 1987.Google Scholar
  69. 69.
    Philip Thambidurai and You-Keun Park. Interactive consistency with multiple failure modes. In 7th Symposium on Reliable Distributed Systems, pages 93–100, Columbus, OH, October 1988. IEEE Computer Society.Google Scholar
  70. 70.
    Time-Triggered Technology TTTech Computertechnik AG, Vienna, Austria. Specification of the TTP/C Protocol (version 0.6p0504), May 2001.Google Scholar
  71. 71.
    Ashish Tiwari, Harald Rueβ, Hassen Saÿdi, and N. Shankar. A technique for invariant generation. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, volume 2031 of Lecture Notes in Computer Science, pages 113–127, Genova, Italy, April 2001. Springer-Verlag.CrossRefGoogle Scholar
  72. 72.
    Charles B. Weinstock and John Rushby, editors. Dependable Computing for Critical Applications-7, volume 12 of Dependable Computing and Fault Tolerant Systems, San Jose, CA, January 1999. IEEE Computer Society.Google Scholar
  73. 73.
    J. Lundelius Welch and N. Lynch. A new fault-tolerant algorithm for clock synchronization. Information and Computation, 77(1):1–36, April 1988.Google Scholar
  74. 74.
    Matthew M. Wilding, David S. Hardin, and David A. Greve. Invariant performance: A statement of task isolation useful for embedded application integration. In Weinstock and Rushby [72], pages 287–300.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • John Rushby
    • 1
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations