Specifying Hardware Timing with ET-Lotos
It is explained how Dill (Digital Logic in Lotos) can specify and analyse hardware timing characteristics using ET-Lotos (Enhanced Timed Lotos — the ISO Language Of Temporal Ordering Specification). Hardware functionality and timing characteristics are rigorously specified and then validated.
KeywordsSetup Time General Delay Digital Logic Input Change Operator Delta
- 1.ISO/IEC. Information Processing Systems-Open Systems Interconnection- Lotos-A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807. International Organization for Standardization, Geneva, Switzerland, 1989.Google Scholar
- 2.Ji He and Kenneth J. Turner. Dill (Digital Logic in Lotos) project web page. http://www.cs.stir.ac.uk/~kjt/research/dill.html, November 2000.
- 3.Luc Léonard and Guy Leduc. An enhanced version of timed Lotos and its application to a case study. In Richard L. Tenney, Paul D. Amer, and M. Ümit Uyar, editors, Proc. Formal Description Techniques VI, pages 483–500. North-Holland, Amsterdam, Netherlands, 1994.Google Scholar
- 4.Luis Llana and Gualberto Rabay Filho. Defining equivalences between time/action graphs and timed action graphs. Technical report, Department of Telematic Systems Engineering, Polytechnic University of Madrid, Spain, December 1995.Google Scholar
- 5.Gualberto Rabay Filho and Juan Quemada. TE-Lola: A timed Lola prototype. In Zmago Brezocnik and Tatjana Kapus, editors, Proc. COST 247 International Workshop on Applied Formal Methods, pages 85–95, Slovenia, June 1996. University of Maribor.Google Scholar