Symbolic Model Checking with Past and Future Temporal Modalities: Fundamentals and AlgorithmsReportar como inadecuado




Symbolic Model Checking with Past and Future Temporal Modalities: Fundamentals and Algorithms - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 TIMA - Techniques of Informatics and Microelectronics for integrated systems Architecture

Abstract : Model checking is gaining importance in verifying the partial specifications of complex synchronous systems modelled by means of a finite state machine. In this paper, we present the principles and a tool for checking their properties in a temporal logic that allows both past and future oriented modalities. After a revision of the basic concepts of the finite state machine model, and of its representation using binary decision diagrams, we present several algorithms to traverse the set of states symbolically. We then extend CTL with past oriented modalities and give properties of this extended temporal logicTL. We give algorithms to verify TL formulas by symbolic model checking. A prototype symbolic model checker for TL, taking as input synchronous circuits written in a VHDL subset, has been implemented.

Keywords : synchronous systems





Autor: D. Deharbe - D. Borrione -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados