Relative timing based verification of concurrent systems
Peña Basurto, Antinisca Di Marco · TDX (Tesis Doctorals en Xarxa) · 2003
La tesi presenta una nova teoria i una metodologia per a la verificacio formal de propietats de seguretat en sistemes temporitzats. El correcte funcionament d'aquests sistemes no nomes depen d'un conjunt de propietats funcionals, sino tambe 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 verificacio d'aquest tipus de sistemes tipicament implica la resolucio de varis problemes computacionalment molt complexes. En concret, la explosio combinatoria d'estats es fa especialment palesa en incloure la dimensio temporal en el problema.La teoria en que es fonamenta el metode de verificacio proposat esten els metodes simbolics convencionals basats en BDDs, per al seu us en la verificacio 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'ocurrencia 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 es suficient comprovar que cert senyal commuta abans que un altre, enlloc d'identificar exactament els instants en que ambdos senyals commuten. Fins i tot, no es necessari calcular la informacio temporal per al sistema complet en el seu conjunt, enlloc d'aixo es pot calcular localment per a la part del sistema relacionada amb la demostracio d'una determinada propietat. Aixo es possible gracies a una observacio crucial:que el conjunt d'execucions d'un sistema de transicions es pot cobrir mitjancant un conjunt d'ordres parcials. En consequencia, per demostrar una propietat nomes es necessari considerar un subconjunt dels esdeveniments del sistema i l'analisi temporal pot fer-se de forma molt eficient.Els metodes convencionals per a la verificacio de sistemes temporitzats es basen en el calcul exacte de l'espai d'estats temporitzat del sistema com a primer pas de l'analisi. Tot i que s'han proposat tecniques eficients per a mitigar la complexitat associada, els metodes d'analisi simbolic no son facilment aplicables. Consequentment, el problema de l'explosio combinatoria de l'espai d'estats temporitzat sovint limita la aplicacio practica dels metodes esmentats a sistemes de tamany moderat.Per altra banda, el metode proposat a la tesi es basa en un refinament incremental de l'espai d'estats no temporitzat del sistema, de forma que la informacio temporal nomes s'incorpora al sistema quan aquesta es fa necessaria. La informacio temporal es deriva a partir d'una analisi 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 representacio eficient del domini temporal d'un sistema tot usant tecniques simboliques convencionals. En consequencia, el metode pot aplicar-se potencialment a sistemes de tamany mes gran o amb mes nivell de detall, que els sistemes que poden verificar-se mitjancant metodes similars. Addicionalment, el fet que el metode proposat sigui incremental proporciona una bona forma d'obtenir al menys resultats parcials fins i tot en sistemes pels que un resultat complet de verificacio fora excessivament complex de calcular.Un aspecte clau del metode de verificacio proposat es que no nomes comprova la correctesa d'un sistema temporitzat. Si el sistema es correcte, la verificacio proporciona un conjunt suficient de relacions temporals relatives que ho demostren. Pel contrari, si el sistema es incorrecte, la verificacio proporciona una traca d'error com a contraexemple. L'aspecte mes interessant de tota aquesta informacio es la seva utilitat al llarg del cicle de disseny d'un sistema. Aquest fet permet mitigar la tradicional distancia entre la verificacio i el disseny, fet que constitueix un altre aspecte diferencial del metode de verificacio proposat envers a altres metodes de verificacio equivalents.El metode de verificacio proposat s'ha implementat completament en una eina de CAV (Verificacio Assistida per Computador) anomenada TRANSYT. L'eina permet manipular sistemes jerarquics i modulars que poden interoperar mitjancant diversos mecanismes de comunicacio. TRANSYT ha demostrat la seva funcionalitat i la validesa del metode de verificacio proposat, mitjancant la verificacio de diversos circuits asincrons temporitzats amb mes de 10E+6 estats no temporitzats. Els experiments realitzats inclouen la verificacio de: descomposicions de portes logiques complexes en circuits asincrons casi-independents-de-la-velocitat, circuits de logica domino, sistemes amb comportaments basats en polsos, circuits optimitzats per a velocitat mitjancant suposicions temporals, etc. Addicionalment, s'ha combinat el metode de verificacio proposat amb metodes de verificacio composicional per tal d'atacar la verificacio de sistemes temporitzats complexes. En aquesta linia, s'han usat tecniques d'abstraccio, raonament del tipus suposicio-garantia i induccio matematica per tal de demostrar la correctesa de l'arquitectura IPCMOS. Aquesta es una arquitectura segmentada i escalable que permet la interconnexio de subsistemes sincrons amb diferents frequencies de rellotge.Gracies al caire teoric del metode de verificacio proposat, el seu potencial d'aplicacio cobreix un rang de sistemes molt mes gran que els esmentats anteriorment, com per exemple: circuits de proposit especific dissenyats a nivell de transistor per tal d'explotar els limits tecnologics i aconseguir un major rendiment, estructures digitals complexes on la sincronitzacio es crucial (e.g. MOS dinamic), sistemes asincrons i del tipus GALS (Globalment Asincron Localment Sincron), sistemes de temps real, etc.