Abstract
In this paper, we propose a technique for hardware implementation of protocol specifications in LOTOS. For the purpose, we define a new model called synchronous EFSMs consisting of concurrent EFSMs and a finite set of multi-rendezvous indications among their subsets, and propose a conversion algorithm from a subset of LOTOS. The derived synchronous EFSMs can be easily implemented as a synchronous sequential circuit where all the modules corresponding to the EFSMs work synchronously with the same clock. By applying our technique to the Abracadabra protocol, it is confirmed that the derived circuit handles multi-rendezvous efficiently.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35394-4_29
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Faci, M. and Logrippo, L.: “Specifying Hardware Systems in LOTOS”, Proc. IFIP Int. Conf on Hardware Description Languages and Applications (CHDL’93): 305–312 (1993).
Higashino, T., Yasumoto, K., Kitamichi, J. and Taniguchi, K.: “Hardware Synthesis from a Restricted Class of LOTOS Expressions”, Proc. 14th IFIP Int. Symp. on Protocol Specification, Testing, and Verification (PSTV-XIV): 355–362 (1994).
ISO: “Information Processing System, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour”, ISO 8807 (1989).
ISO/IEC/TR 10167: “Information Technology — Open Systems Interconnection — Guidelines for the application of Estelle, LOTOS and SDL” (1991).
Kitajima, A., Yasumoto, K., Higashino, T. and Taniguchi, K.: “A Method to Convert Concurrent EFSMs with Multi-Rendezvous into Synchronous Sequential Circuits”, IEICE Trans. on Fundamentals, E81-A (4): 566–575 (1998).
Kloos, C. D. and Damm, W. (Eds.): “Practical Formal Methods for Hardware Design”, Research Reports Esprit, Project 6128, FORMAT, Vol. 1, Springer (1996).
Lopez, A. M., Kloos, C. D., Valladares, T. R. and Moro, T. M.: “Generating VHDL code from LOTOS Descriptions”, in [6]: 266–293 (1996).
Nakamura, Y.: “An Integrated Logic Design Environment Based on Behavioral Description”, IEEE Trans. on CAD, CAD-6 (3): 322–336 (1987).
Ott, D. E. and Wilderotter, T. J.: `A Designer’s Guide to VHDL Synthesis“, Kluwer Academic Publishers (1994).
Quemada, J., Larrabeiti, D. and Pavon, S.: “Compressing the State Space Representation of LOTOS Specifications”, Proc. 6th IFIP Int. Conf. on Formal Description Techniques (FORTE’93): 19–34 (1993).
Sisto, R.: “A method to build symbolic representations of LOTOS specifications”, Proc. 15th IFIP Int. Symp. on Protocol Specification, Testing and Verification (PSTV-XV): 331–346 (1995).
Turner, K. J. and Sinnott, R. O.: “DILL: Specifying Digital Logic in LOTOS”, Proc. 6th IFIP Formal Description Techniques (FORTE’93) (1994).
Csopaki, G. and Turner, K. J.: “Modelling Digital Logic in SDL”: Proc. Joint Int. Conf. on Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE/PSTV’97): 367–382 (1997).
Vissers, C. A., Scollo, G. and Sinderen, M. v.: “Architecture and Specification Style in Formal Descriptions of Distributed Systems”, Proc. 8th Int. Symp. on Protocol Specification, Testing, and Verification (PSTV-VIII): 189–204 (1988).
Wytrebowicz, J.: “Hardware Specification Generated from Estelle”, Proc.. 15th IFIP Int. Symp. on Protocol Specification, Testing and Verification (PSTV-XV): 435–450 (1996).
Yasumoto, K.: “A method to derive concurrent synchronous EFSMs from protocol specifications in LOTOS”, Tech. Rep. # 1113 of Dept. IRO, University of Montreal (1998).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Yasumoto, K., Kitajima, A., Higashino, T., Taniguchi, K. (1998). Hardware Synthesis from Protocol Specifications in LOTOS. In: Budkowski, S., Cavalli, A., Najm, E. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. PSTV FORTE 1998 1998. IFIP — The International Federation for Information Processing, vol 6. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35394-4_25
Download citation
DOI: https://doi.org/10.1007/978-0-387-35394-4_25
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5262-5
Online ISBN: 978-0-387-35394-4
eBook Packages: Springer Book Archive