Specification of Embedded Monitors for Property Checking
The development of new application domains in the telecom market, such as mobile telephony or multimedia services, has led to a substantial increase in the average complexity of single devices. This complexity makes the definition and verification of the interoperability of different modules in a system a very error prone task. Formal verification techniques are becoming more and more attractive as part of the verification methodology, in conjunction to simulation, to guarantee the complete correctness of complex devices. Several examples of applications in industrial environments of these techniques [7,6,1] show that they have reached an acceptable level of maturity. Still, problems of complexity handling imposed by today’s model checking technology  limit for the moment a wider diffusion.
KeywordsFormal Verification Device Model Read Operation Virtual State Rigid Variable
Unable to display preview. Download preview PDF.
- A. Allara, C. Bolchini, P. Cavalloro, S. Cornai, Guidelines for Property Verification of VHDL Models: an Industrial Perspective, FDL’98, Lausanne, Switzerland, 6–11 Sept. 1998, pp. 11–20Google Scholar
- A. Allara, S. Cornai, R. Schlör, System Verification Using User-friendly Interfaces, DATE’99, Munich, Germany, March 1999.Google Scholar
- W. Damm, B. Josko, R. Schlör, Specification and Verification of (VHDL)-based System-Level Hardware Designs, Specification and Validation Methods, ed. E. Börger, Oxford University Press, pp. 331–410, 1995.Google Scholar
- R. Schlör and W. Damm. Specification and verification of system-level hardware designs using timing diagrams. In Proc. The European Conf. on Design Automation, pp. 518–524, Paris, France, IEEE Computer Society Press, 1993.Google Scholar
- R. Schlör, B. Josko, D. Werth, Using a visual formalism for design verification in industrial environments, TACAS’98, LNCS, Springer-Verlag, 1998.Google Scholar
- J. Y. Jang, S. Qadeer, M. Kaufmann, C. Pixley, Formal Verification of FIRE: A Case Study, 34th DAC, proceeding 1997Google Scholar
- B. Plessier, C. Pixley, Formal Verification of a Commercial Serial Bus Interface, Int’I Conf. on Computers and Communications, Phoenix, USA, pp. 378–382, 1995Google Scholar
- M. D. Aegaard, R. B. Jones, C. H. Seger, Combining Theorem Proving and Trajectory Evaluation in a Industrial Environment, 35th DAC, San Francisco, USA, pp 538–541, 1998Google Scholar
- K. Feyerabend, B. Josko, A Visual Formalism for Real Time Requirement Specifications, in Proc. Transformation-Based Reactive Systems Development, ARTS’97, LNCS 1231, pp. 156–168, Springer-Verlag, 1997.Google Scholar