Relative timing based verification of concurrent systems

La tesi presenta una nova teoria i una metodologia per a la verificació formal de propietats de seguretat en sistemes temporitzats. El correcte funcionament d'aquests sistemes no només depèn d'un conjunt de propietats funcionals, sinó també de certes suposicions sobre els retards dels components del sistema i els temps de resposta de l'entorn en el que opera el sistema. La verificació d'aquest tipus de sistemes típicament implica la resolució de varis problemes computacionalment molt complexes. En concret, la explosió combinatòria d'estats es fa especialment palesa en incloure la dimensió temporal en el problema.La teoria en que es fonamenta el mètode de verificació proposat estén els mètodes simbòlics convencionals basats en BDDs, per al seu ús en la verificació de sistemes temporitzats modelats usant sistemes de transicions temporitzats. La teoria es basa en el paradigma de les relacions temporals relatives, que enlloc de considerar els temps exactes d'ocurrència dels esdeveniments, considera l'efecte dels retards en termes d'ordenacions relatives entre esdeveniments. Per exemple, per garantir que una carrera no se propaga en un circuit digital, sovint és suficient comprovar que cert senyal commuta abans que un altre, enlloc d'identificar exactament els instants en que ambdós senyals commuten. Fins i tot, no és necessari calcular la informació temporal per al sistema complet en el seu conjunt, enlloc d'això es pot calcular localment per a la part del sistema relacionada amb la demostració d'una determinada propietat. Això és possible gràcies a una observació crucial:que el conjunt d'execucions d'un sistema de transicions es pot cobrir mitjançant un conjunt d'ordres parcials. En conseqüència, per demostrar una propietat només és necessari considerar un subconjunt dels esdeveniments del sistema i l'anàlisi temporal pot fer-se de forma molt eficient.Els mètodes convencionals per a la verificació de sistemes temporitzats es basen en el càlcul exacte de l'espai d'estats temporitzat del sistema com a primer pas de l'anàlisi. Tot i que s'han proposat tècniques eficients per a mitigar la complexitat associada, els mètodes d'anàlisi simbòlic no són fàcilment aplicables. Conseqüentment, el problema de l'explosió combinatòria de l'espai d'estats temporitzat sovint limita la aplicació pràctica dels mètodes esmentats a sistemes de tamany moderat.Per altra banda, el mètode proposat a la tesi es basa en un refinament incremental de l'espai d'estats no temporitzat del sistema, de forma que la informació temporal només s'incorpora al sistema quan aquesta es fa necessària. La informació temporal es deriva a partir d'una anàlisi temporal eficient sobre petits conjunts d'esdeveniments. L'espai d'estats refinat es captura sota el model dels sistemes de transicions mandrosos, que permeten la representació eficient del domini temporal d'un sistema tot usant tècniques simbòliques convencionals. En conseqüència, el mètode pot aplicar-se potencialment a sistemes de tamany més gran o amb més nivell de detall, que els sistemes que poden verificar-se mitjançant mètodes similars. Addicionalment, el fet que el mètode proposat sigui incremental proporciona una bona forma d'obtenir al menys resultats parcials fins i tot en sistemes pels que un resultat complet de verificació fóra excessivament complex de calcular.Un aspecte clau del mètode de verificació proposat es que no només comprova la correctesa d'un sistema temporitzat. Si el sistema és correcte, la verificació proporciona un conjunt suficient de relacions temporals relatives que ho demostren. Pel contrari, si el sistema és incorrecte, la verificació proporciona una traça d'error com a contraexemple. L'aspecte més interessant de tota aquesta informació és la seva utilitat al llarg del cicle de disseny d'un sistema. Aquest fet permet mitigar la tradicional distància entre la verificació i el disseny, fet que constitueix un altre aspecte diferencial del mètode de verificació proposat envers a altres mètodes de verificació equivalents.El mètode de verificació proposat s'ha implementat completament en una eina de CAV (Verificació Assistida per Computador) anomenada TRANSYT. L'eina permet manipular sistemes jeràrquics i modulars que poden interoperar mitjançant diversos mecanismes de comunicació. TRANSYT ha demostrat la seva funcionalitat i la validesa del mètode de verificació proposat, mitjançant la verificació de diversos circuits asíncrons temporitzats amb més de 10E+6 estats no temporitzats. Els experiments realitzats inclouen la verificació de: descomposicions de portes lògiques complexes en circuits asíncrons casi-independents-de-la-velocitat, circuits de lògica dominó, sistemes amb comportaments basats en polsos, circuits optimitzats per a velocitat mitjançant suposicions temporals, etc. Addicionalment, s'ha combinat el mètode de verificació proposat amb mètodes de verificació composicional per tal d'atacar la verificació de sistemes temporitzats complexes. En aquesta línia, s'han usat tècniques d'abstracció, raonament del tipus suposició-garantia i inducció matemàtica per tal de demostrar la correctesa de l'arquitectura IPCMOS. Aquesta és una arquitectura segmentada i escalable que permet la interconnexió de subsistemes síncrons amb diferents freqüències de rellotge.Gràcies al caire teòric del mètode de verificació proposat, el seu potencial d'aplicació cobreix un rang de sistemes molt més gran que els esmentats anteriorment, com per exemple: circuits de propòsit específic dissenyats a nivell de transistor per tal d'explotar els límits tecnològics i aconseguir un major rendiment, estructures digitals complexes on la sincronització és crucial (e.g. MOS dinàmic), sistemes asíncrons i del tipus GALS (Globalment Asíncron Localment Síncron), sistemes de temps real, etc.La tesis presenta una nueva teoría y una metodología para la verificación formal de propiedades de seguridad en sistemas temporizados. El correcto funcionamiento de estos sistemas no sólo depende de un conjunto de propiedades funcionales sino también de ciertas suposiciones sobre los retardos de los componentes del sistema y los tiempos de respuesta del entorno en el que opera el sistema. La verificación de este tipo de sistemas típicamente implica la resolución de varios problemas computacionalmente muy complejos. En concreto, la explosión combinatoria de estados se hace especialmente patente al incluir la dimensión temporal en el problema.La teoría en que se sustenta el método de verificación propuesto extiende los métodos simbólicos convencionales basados en BDDs, para su uso en la verificación de sistemas temporizados modelados usando sistemas de transiciones temporizados. La teoría se basa en el paradigma de las relaciones temporales relativas, que en lugar de considerar los tiempos exactos de ocurrencia de los eventos, considera el efecto de los retardos en términos de ordenaciones relativas entre eventos. Por ejemplo, para garantizar que una carrera no se propaga en un circuito digital, a menudo es suficiente comprobar que cierta señal conmuta antes que otra, en lugar de identificar exactamente los instantes en que ambas señales conmutan. Es más, no es necesario computar la información temporal para el sistema completo en su conjunto, si no sólo localmente para la parte del sistema relacionada con la demostración de una determinada propiedad. Esto es posible gracias a una observación crucial: que el conjunto de ejecuciones de un sistema de transiciones puede cubrirse por un conjunto de órdenes parciales. En consecuencia, para la demostración de una propiedad sólo es necesario considerar un subconjunto de los eventos del sistema y el análisis temporal puede hacerse de forma muy eficiente. Los métodos convencionales para la verificación de sistemas temporizados se basan en el cálculo exacto del espacio de estados temporizado del sistema como primer paso del análisis. Aunque se han propuesta técnicas eficientes para paliar la complejidad asociada, los métodos de análisis simbólico no son fácilmente aplicables. Consecuentemente, el problema de la explosión combinatoria del espacio de estados temporizado a menudo limita la aplicación práctica de dichos métodos a sistemas de tamaño moderado.Por el contrario, el método propuesto en la tesis se basa en un refinamiento incremental del espacio de estados no temporizado del sistema, de forma que la información temporal sólo se incorpora al sistema cuando ésta se hace necesaria. Dicha información temporal se deriva a partir de un análisis temporal eficiente sobre pequeños conjuntos de eventos. El espacio de estados refinado se captura bajo el modelo de los sistemas de transiciones perezosos, que permiten la representación eficiente del dominio temporal de un sistema usando técnicas simbólicas convencionales. En consecuencia, el método puede aplicarse potencialmente a sistemas de mayor tamaño o con mayor nivel de detalle, que los sistemas que pueden verificarse con métodos similares. Adicionalmente, la naturaleza incremental del método propuesto proporciona una buena forma de obtener al menos resultados parciales incluso en sistemas para los cuales un resultado completo de verificación seria excesivamente complejo de calcular.Un aspecto clave del método de verificación propuesto es que no sólo comprueba la corrección de un sistema temporizado. Si el sistema es correcto, la verificación proporciona un conjunto suficiente de relaciones temporales relativas que lo demuestran. Por el contrario, si el sistema es incorrecto, la verificación proporciona una traza de error a modo de contraejemplo. El aspecto más interesante de toda esta información es su utilidad a lo largo del ciclo de diseño de un sistema. Este hecho permite mitigar la tradicional distancia entre la verificación y el diseño en sí, lo que constituye otro aspecto diferencial del método de verificación propuesto frente a otros métodos de verificación equivalentes.El método de verificación propuesto se ha implementado completamente en una herramienta de CAV (Verificación Asistida por Computador) llamada TRANSYT. La herramienta permite manipular sistemas jerárquicos y modulares los cuales pueden interoperar mediante varios mecanismos de comunicación. TRANSYT ha demostrado su funcionalidad así como la validez del método de verificación propuesto, mediante la verificación de diversos circuitos asíncronos temporizados con más de 10E+6 estados no temporizados. Los experimentos realizados incluyen la verificación de: descomposiciones de puertas lógicas complejas en circuitos asíncronos casi-independientes-de-la-velocidad, circuitos de lógica dominó, sistemas con comportamientos basados en pulsos, circuitos optimizados para velocidad mediante suposiciones temporales, etc. Adicionalmente, se ha combinado el método de verificación propuesto con métodos de verificación composicional con el fin de atacar la verificación de sistemas temporizados complejos. En esta línea, se han usado técnicas de abstracción, razonamiento del tipo suposición-garantía e inducción matemática para demostrar la corrección de la arquitectura IPCMOS. Ésta es una arquitectura segmentada y escalable que permite la interconexión de subsistemas síncronos con diferentes frecuencias de reloj.Gracias a la naturaleza teórica del método de verificación propuesto, su potencial de aplicación cubre un rango de sistemas mucho mayor a los citados anteriormente, como por ejemplo: circuitos de propósito específico diseñados a nivel de transistor para explotar los límites tecnológicos en pro de un mayor rendimiento, estructuras digitales complejas en las que la sincronización es crucial (e.g. MOS dinámico), sistemas asíncronos y del tipo GALS (Globalmente Asíncrono Localmente Síncrono), sistemas de tiempo real, etc.The thesis presents a new theory and methodology for the formal verification of safety properties in timed systems. The correct operation of such systems not only depends on a set of functional properties but also on certain assumptions about the delays of the components of the system and the response times of the environment in which the system operates. The verification of this type of systems typically involves several computationally hard problems. In particular, the combinatorial state explosion problem becomes exacerbated by the time dimension.The theory that supports the proposed verification approach extends the conventional BDD-based symbolic methods to the verification of timed systems, modeled by means of timed transition systems. The theory is based on the relative timing paradigm, which instead of considering exact time differences in the occurrence of events, considers the effect of delays in terms of relative orderings between events. For example, in order to guarantee that a race is not propagated in a digital circuit, it is often sufficient to check that certain signal switches before another, instead of identifying the exact instants of time in which both signals switch. Moreover, the timing information does not need to computed for the overall system, but only locally for the part of the system involved in the proof or disproof of a given property. This is possible thanks to a crucial observation, that the set of executions of a transition system can be covered by a set of partial orders. As a consequence, only a subset of the events of the system is involved in the proof of a property and the timing analysis can be carried out very efficiently. Conventional methods for the verification of timed systems rely on the computation of the exact timed state space of the system as the first step of the analysis. Although efficient techniques have been devised to overcome the complexity issue (e.g. difference bound matrices), symbolic methods cannot be easily applied. Thus, the combinatorial time-state explosion problem often limits the applicability of such methods to moderate-size systems. Instead, the approach proposed in the thesis relies on an incremental refinement of the untimed state space of the system, so that timing information is incorporated as soon as it is needed. The timing information is derived by an efficient off-line timing analysis over small sets of events. The refined state space is captured under the model of lazy transition system, which allows an efficient representation of the timed domain using conventional symbolic methods. As a consequence, the approach can be potentially applied to bigger systems or to systems with more level of detail, than those that can be handled by similar methods for the verification of timed systems. Moreover, the incremental nature of the approach provides a good way to obtain at least partial results even on systems for which complete solutions could be too complex to compute. A key feature of the proposed verification approach is that not only proves or disproves the correctness of a timed system. If the system is correct the set of relative timing relations used for the proof are provided. Such relations constitute a set of sufficient timing constraints that guarantee the correctness of the system. On the other hand, if the system is incorrect, a counterexample failure trace is provided. The most important aspect of all this feedback is that it can be used as valuable back-annotation information along the design process.This feature, which allows to bridge the gap between verification and design, constitutes another differential aspect of our verification approach when compared to other equivalent verification methods. The verification approach has been fully implemented in an experimental CAV tool called TRANSYT. The tool can handle hierarchical and distributed modular systems which can inter-operate by a variety of communication mechanisms. TRANSYT has successfully proved its functionality as well as the validity of the overall verification approach, by verifying a number of timed asynchronous circuits with up to more than 10E+6 untimed states.The experiments cover, for example, the verification of: complex-gate decompositions in quasi-speed-independent asynchronous circuits, delay-reset domino circuits, pulse-based systems, circuits optimized for speed using timing assumptions, etc. Additionally, compositional verification methods have been combined with the basic verification approach in order to tackle the size/complexity issues involved in the verification of complex timed systems. Thus, abstractions, assume-guarantee reasoning and mathematical induction have been used to prove the correctness the IPCMOS architecture. It is a scalable pipelined architecture which is aimed to the interconnection of different clock zones in a system. Thanks to the rather theoretical nature of the proposed verification approach, its potential applicability covers a wider range of systems than those cited above, such as: custom transistor-level circuits that exploit the technology limits for performance, complex digital structures where synchronization is a crucial issue (e.g. dynamic MOS), asynchronous and GALS-type systems, real-time systems, etc.Postprint (published version