Abstract
A formal method of synthesising a converter that translates signals between two heterogeneous, off-the-shelf protocol IPs is presented in the form of a case study. At the heart of the method is a model checker that guarantees the converter satisfies correctness conditions, as well as user-defined properties. In this approach, the issue of nondeterminism is explicitly addressed, and is used to synthesise an optimal converter.
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
Akella, J., McMillan, K.L.: Synthesizing converters between finite state protocols. In: Computer Design on VLSI in Computer & Processors, pp. 410–413. IEEE, Los Alamitos (1991)
Avnit, K., D’Silva, V., Sowmya, A., Ramesh, S., Parameswaran, S.: A formal approach to the protocol converter problem. In: Proceedings of the conference on Design, automation and test in Europe (DATE 2008), pp. 294–299. ACM, New York (2008)
Sinha, R., Roop, P.S., Basu, S.: A model checking approach to protocol conversion. Electr. Notes Theor. Comput. Sci. 203(4), 81–94 (2008)
Passerone, R., de Alfaro, L., Henzinger, T., Sangiovanni-Vincentelli, A.: Convertibility verification and converter synthesis: two faces of the same coin. In: International Conference on Computer Aided Design, November 2002, pp. 132–139 (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
ARM: AMBA Specification (Rev. 2) (May 1999), www.gaisler.com/doc/amba.pdf
Cao, J., Nymeyer, A.: Formal model of a protocol converter. In: Fifteenth Computing: The Australasian Theory Symposium. CRPIT, vol. 94, pp. 107–117 (2009)
Cao, J., Nymeyer, A.: Formal, correct and optimal component reuse. In: United international systems conference (Uniscon 2009) (to be published, 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cao, J., Nymeyer, A. (2009). Formally Synthesising a Protocol Converter: A Case Study. In: Maneth, S. (eds) Implementation and Application of Automata. CIAA 2009. Lecture Notes in Computer Science, vol 5642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02979-0_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-02979-0_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02978-3
Online ISBN: 978-3-642-02979-0
eBook Packages: Computer ScienceComputer Science (R0)