Parametric Verification of a Group Membership Algorithm

  • Ahmed Bouajjani
  • Agathe Merceron
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


We address the problem of verifying clique avoidance in the TTP protocol. TTP allows several stations embedded in a car to communicate. It has many mechanisms to ensure robustness to faults. In particular, it has an algorithm that allows a station to recognize itself as faulty and leave the communication. This algorithm must satisfy the crucial ’non-clique’ property: it is impossible to have two or more disjoint groups of stations communicating exclusively with stations in their own group. In this paper, we propose an automatic verification method for an arbitrary number of stations N and a given number of faults k. We give a faithful abstraction that allows to model the algorithm by means of unbounded (parametric) counter automata. We have checked the non-clique property on this model in the case of one fault, using the ALV tool as well as the LASH tool.


Formal verification fault-tolerant protocols parametric counter automata abstraction 


  1. 1.
    Abdulla P.A, Annichini A., Bensalem S., Bouajjani A., Habermehl P., Lakhnech Y: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. CAV’99, Lecture Notes in Computer Science, Vol 1633. Springer-Verlag, (1999)Google Scholar
  2. 2.
    Abdulla P.A, Jonsson B.: Channel Representations in Protocol Verification. CON-CUR’01, Lecture Notes in Computer Science, Vol 2154. Springer-Verlag, (2001) 1–15Google Scholar
  3. 3.
    Abdulla P.A, Jonsson B.: Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems. Theoretical Computer Science, Vol 256. (2001) 145–167zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Annichini A., Asarin E., Bouajjani A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. CAV’00, Lecture Notes in Computer Science, Vol 1855. (2000)Google Scholar
  5. 5.
    Bauer G., Paulitsch M.: An investigation of membership and clique avoidance in TTP/C. Proceedings 19th IEEE Symposium on Reliable Distributed Systems (SRDS’00), IEEE Computer Society, (2000), 118–124Google Scholar
  6. 6.
    Baukus K., Lakhnech Y., Stahl K.: Verifying Universal Properties of Parameterized Networks. Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 2000, Pune, IndiaGoogle Scholar
  7. 7.
    Boigelot B., Wolper P.: Symbolic Verification with Periodic Sets. CAV’94, Lecture Notes in Computer Science, Vol 818. Springer-Verlag, (1994)Google Scholar
  8. 8.
    Bouajjani A., Esparza J., Maler O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. CONCUR’97, Lecture Notes in Computer Science, Vol 1243. Springer-Verlag, (1997)Google Scholar
  9. 9.
    Bouajjani A., Habermehl P.: Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. ICALP’97, Lecture Notes in Computer Science, Vol 1256. Springer-Verlag, (1997) Full version in TCS, Vol 221 (1/2) (1999) 221–250Google Scholar
  10. 10.
    Bouajjani A., Jonsson B., Nilsson M., Touili T.: Regular Model Checking. CAV’00, Lecture Notes in Computer Science, Vol 1855. Springer-Verlag, (2000)Google Scholar
  11. 11.
    Bouajjani A., Merceron A.: Parametric Verification of a Group Membership Algorithm. Technical Report, Liafa, University of Paris 7, (2002)Google Scholar
  12. 12.
    Bultan T., Gerber R., League C.: Verifying Systems With Integer Constraints and Boolean Predicates: A Composite Approach. Proc. of the Intern. Symp. on Software Testing and Analysis, ACM Press (1998)Google Scholar
  13. 13.
    Bultan T., Yavuz-Kahveci T.: Action Language Verifier. Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), IEEE Computer Society, Coronado Island, California, (2001)Google Scholar
  14. 14.
    Cousot P., Halbwachs H.: Automatic Discovery of Linear Restraints Among Variables of a Program. POPL’78, ACM Press (1978)Google Scholar
  15. 15.
    Creese S., Roscoe A.W.: TTP: a case study in combining induction and data independence. Oxford University Programming Research Group, Technical Report TR-1-99, (1999)Google Scholar
  16. 16.
    Graf S., Saidi H.: Construction of abstract state graphs with pvs. CAV’97, Lecture Notes in Computer Science, Vol 1254. Springer-Verlag, (1997)Google Scholar
  17. 17.
    Katz S., Lincoln P., Rushby J.: Low-overhead Time-Triggered Group Membership. WDAG’97, Lecture Notes in Computer Science, Vol 1320. Springer-Verlag, (1997)Google Scholar
  18. 18.
    Kesten Y., Maler O., Marcus M., Pnueli A., Shahar E.: Symbolic Model Checking with Rich Assertional Languages. CAV’97, Lecture Notes in Computer Science, Vol 1254. Springer-Verlag, (1997)Google Scholar
  19. 19.
    Kopetz H.: TTP/C Protocol-Specification of the TTP/C Protocol. (1999)
  20. 20.
    Kopetz H., Grünsteidl G.: A time triggered protocol for fault-tolerant Real-Time Systems. IEEE Computer, (1999) 14–23Google Scholar
  21. 21.
    LASH: The Liége Automata-based Symbolic Handler (LASH).
  22. 22.
    Pfeifer H.: Formal verification of the TTP Group Membership Algorithm. IFIP TC6/WG6.1 International Conference on Formal Description Techniques for Distributed Systems and Communication protocols and Protocol Specification, Testing and Verification, FORTE/PSTV 2000, Pisa, Italy (2000)Google Scholar
  23. 23.
    Saidi H., Shankar N.: Abstract and Model Check while you Prove. CAV’99, Lecture Notes in Computer Science, Vol 1633. Springer-Verlag, (1999)Google Scholar
  24. 24.
    Wolper W., Boigelot B.: Verifying systems with infinite but regular state spaces. CAV’98, Lecture Notes in Computer Science, Vol 1427. Springer-Verlag, (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Ahmed Bouajjani
    • 1
  • Agathe Merceron
    • 1
  1. 1.LiafaUniv. of Paris 7Paris 5France

Personalised recommendations