Abstract
The development of safety-critical embedded applications in domains such as automotive or avionics is an exceedingly challenging intellectual task. This task can, however, be significantly simplified through the use of middleware that offers specialized fault-tolerant services. This middleware must provide a high assurance level that it operates correctly. In this paper, we present a formal verification of a protocol for one such service, a Group Membership Service, using model checking. Through this verification we discovered that although the protocol specification is correct, a previously proposed implementation is not.
Sponsored by scholarship from FCT foundation under reference number SFRH/BD 19302/2004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Rushby, J.M.: Bus Architectures for Safety-Critical Embedded Systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 306–323. Springer, Heidelberg (2001)
Makowitz, R., Temple, C.: FlexRay - A Communication Network for Automotive Control Systems. In: WFCS. 6th IEEE International Workshop on Factory Communication Systems (2006)
Rosset, V., Souto, P., Vasques, F.: A Group Membership Protocol for Communication Systems with both Static and Dynamic Scheduling. In: WFCS. 6th IEEE International Workshop on Factory Communication Systems, Torino, Italy, pp. 28–30 (2006)
Ip, C., Dill, D.: Better Verification through Symmetry. In: International Conference on Computer Hardware Description Languages, pp. 87–100 (April 1993)
Schiper, S., Toueg, A.: From Set Membership to Group Membership: A Separation of Concerns. IEEE Transactions on Dependable and Secure Computing 3(1), 2–12 (2006)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) Hybrid Systems III. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Yovine, S.: Model Checking Timed Automata. In: Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems, pp. 114–152. Springer, London, UK (1998)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems. LNCS, vol. 3185, Springer, Heidelberg (2004)
Bernadeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Software Testing, Verification and Reliability 12, 251–275 (2002)
Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vandraager, F.: Adding Symmetry Reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rosset, V., Souto, P.F., Vasques, F. (2007). Formal Verification of a Group Membership Protocol Using Model Checking. In: Meersman, R., Tari, Z. (eds) On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE, GADA, and IS. OTM 2007. Lecture Notes in Computer Science, vol 4803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76848-7_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-76848-7_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76846-3
Online ISBN: 978-3-540-76848-7
eBook Packages: Computer ScienceComputer Science (R0)