Abstract
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.
This work was supported in part by the European Commission (FET project ADVANCE, contract No IST-1999-29082).
Chapter PDF
References
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)
Abdulla P.A, Jonsson B.: Channel Representations in Protocol Verification. CON-CUR’01, Lecture Notes in Computer Science, Vol 2154. Springer-Verlag, (2001) 1–15
Abdulla P.A, Jonsson B.: Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems. Theoretical Computer Science, Vol 256. (2001) 145–167
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)
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–124
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, India
Boigelot B., Wolper P.: Symbolic Verification with Periodic Sets. CAV’94, Lecture Notes in Computer Science, Vol 818. Springer-Verlag, (1994)
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)
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–250
Bouajjani A., Jonsson B., Nilsson M., Touili T.: Regular Model Checking. CAV’00, Lecture Notes in Computer Science, Vol 1855. Springer-Verlag, (2000)
Bouajjani A., Merceron A.: Parametric Verification of a Group Membership Algorithm. Technical Report, Liafa, University of Paris 7, (2002)
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)
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)
Cousot P., Halbwachs H.: Automatic Discovery of Linear Restraints Among Variables of a Program. POPL’78, ACM Press (1978)
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)
Graf S., Saidi H.: Construction of abstract state graphs with pvs. CAV’97, Lecture Notes in Computer Science, Vol 1254. Springer-Verlag, (1997)
Katz S., Lincoln P., Rushby J.: Low-overhead Time-Triggered Group Membership. WDAG’97, Lecture Notes in Computer Science, Vol 1320. Springer-Verlag, (1997)
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)
Kopetz H.: TTP/C Protocol-Specification of the TTP/C Protocol. http://www.tttech.com (1999)
Kopetz H., Grünsteidl G.: A time triggered protocol for fault-tolerant Real-Time Systems. IEEE Computer, (1999) 14–23
LASH: The Liége Automata-based Symbolic Handler (LASH). http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
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)
Saidi H., Shankar N.: Abstract and Model Check while you Prove. CAV’99, Lecture Notes in Computer Science, Vol 1633. Springer-Verlag, (1999)
Wolper W., Boigelot B.: Verifying systems with infinite but regular state spaces. CAV’98, Lecture Notes in Computer Science, Vol 1427. Springer-Verlag, (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Merceron, A. (2002). Parametric Verification of a Group Membership Algorithm. In: Damm, W., Olderog, E.R. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2002. Lecture Notes in Computer Science, vol 2469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45739-9_19
Download citation
DOI: https://doi.org/10.1007/3-540-45739-9_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44165-6
Online ISBN: 978-3-540-45739-8
eBook Packages: Springer Book Archive