Abstract
We present a tool that automatically checks the existence of a bisimulation relation between an SDL specification and the corresponding auto-generated C code. The tool has been used to verify part of the C implementation of a WiFi Medium Access Controller (IEEE 802.11) that has been derived from its original SDL specification using the Telelogic CAdvanced Code Generator.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Olsen, A., Faergemand, O., Reed, R., Smith, J.R.W., Mller-Pedersen, B.: Systems Engineering Using SDL-92. Elsevier Science, Amsterdam (1994)
Sipilä, J., Luukkala, V.: An SDL Implementation Framework for Third Generation Mobile Communications System. Nokia Research Center, Mobile Networks Laboratory (2001)
Hannikainen, M., Knuutila, J., Hamalainen, T., Saarinen, J.: SDL-to-C Conversion for implementing Embedded Wireless LAN Protocols. IEEE Journal 2000 (2000)
Sidorova, N., Steffen, M.: Verifying Large SDL Specifications Using Model Checking. 10th International SDL-Forum 2001 (2001)
Haroud, M., Blažević, L., Biere, A.: HW accelerated Ultra Wide Band MAC protocol using SDL and SystemC. In: Radio And Wireless Conference 2004 (2004)
Whittaker, J.A.: What Is Software Testing? And Why Is It so Hard? IEEE Software (2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation Validation TACAS 1998 (1998)
Pnueli, A., Siegel, M., Strichman, O.: Translation validation: From SIGNAL to C. Correct System Design 1999 (1999)
Necula, G.C.: Translation validation for an optimizing compiler. ACM sigplan notices 2000 (2000)
Daniel, K., Edmund, C., Karen, Y.: Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking DAC 2003 (2003)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking Advances in Computers Academic press 2003 (2003)
Clarke, Biere, Raimi, Zhu: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design Kluwer Academic Publishers 2001 (2001)
Marsha Chechik Hai: Bisimulation Analysis of SDL-Expressed Protocols: A Case Study. In: CASCON Conference (2000)
Milner, R.: A Calculus of Communicating Systems. Secaucus. Springer, New York (1982)
Horwitz, S., Prins, J., Reps, T.: On the Adequacy of Program Dependence Graphs for Representing Programs Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages 1988 (1988)
Namballa, R., Ranganathan, N.: Control and Data Flow Graph Extraction for High-Level Synthesis Symposium on VLSI Emerging Trends in VLSI Systems Design ISVLSI 2004 (2004)
de Alfaro, L., Henzinger, T.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 148. Springer, Heidelberg (2001)
Ellervee, P., et al.: IRSYD: An internal representation for heterogeneous embedded systems. In: Proceedings of the 16th NORCHIP Conference (1998)
Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. Computer Aided Verification 2001 (2001)
Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specifications High-speed Physical Layer in the 5 GHz band grouper.ieee.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haroud, M., Biere, A. (2005). SDL Versus C Equivalence Checking. In: Prinz, A., Reed, R., Reed, J. (eds) SDL 2005: Model Driven. SDL 2005. Lecture Notes in Computer Science, vol 3530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11506843_23
Download citation
DOI: https://doi.org/10.1007/11506843_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26612-9
Online ISBN: 978-3-540-31539-1
eBook Packages: Computer ScienceComputer Science (R0)