Comprovació de models

En informàtica, la verificació de models o de propietats és un mètode per comprovar si un model d'estat finit d'un sistema compleix una especificació determinada (també coneguda com a correcció). Normalment, això s'associa amb sistemes de maquinari o programari, on l'especificació conté requisits de vida (com ara l'evitació de livelock ) així com requisits de seguretat (com evitar estats que representen una fallada del sistema).

Per tal de resoldre aquest problema algorítmicament, tant el model del sistema com la seva especificació es formulen en un llenguatge matemàtic precís. Amb aquesta finalitat, el problema es formula com una tasca en lògica, és a dir, comprovar si una estructura satisfà una fórmula lògica determinada. Aquest concepte general s'aplica a molts tipus de lògica i molts tipus d'estructures. Un problema simple de verificació de models consisteix a verificar si una fórmula de la lògica proposicional és satisfeta per una estructura determinada.

Visió general

La comprovació de propietat s'utilitza per a la verificació quan dues descripcions no són equivalents. Durant el perfeccionament, l'especificació es complementa amb detalls que no són necessaris a l'especificació de nivell superior. No cal verificar les propietats recentment introduïdes amb l'especificació original, ja que això no és possible. Per tant, l'estricta comprovació d'equivalència bidireccional es relaxa a una comprovació de propietat unidireccional. La implementació o disseny es considera un model del sistema, mentre que les especificacions són propietats que el model ha de satisfer.^[1]

S'ha desenvolupat una classe important de mètodes de verificació de models per comprovar models de dissenys de maquinari i programari on l'especificació ve donada per una fórmula lògica temporal. El treball pioner en l'especificació de la lògica temporal va ser realitzat per Amir Pnueli, que va rebre el premi Turing 1996 per "un treball seminal introduint la lògica temporal a la ciència de la computació".^[2] La comprovació de models va començar amb el treball pioner d'EM Clarke, EA Emerson, de JP Queille i J. Sifakis. Clarke, Emerson i Sifakis van compartir el premi Turing 2007 pel seu treball fonamental fundant i desenvolupant el camp de la verificació de models.^[3]

La comprovació de models s'aplica amb més freqüència als dissenys de maquinari. Per al programari, a causa de la indecidibilitat (vegeu teoria de la computabilitat) l'enfocament no pot ser totalment algorítmic, aplicar-se a tots els sistemes i donar sempre una resposta; en el cas general, pot no acreditar o desmentir una propietat determinada. En el maquinari de sistemes encastats, és possible validar una especificació lliurada, per exemple, mitjançant diagrames d'activitat UML ^[4] o xarxes de Petri interpretades per control.

L'estructura s'acostuma a donar com a descripció del codi font en un llenguatge de descripció de maquinari industrial o un llenguatge de propòsit especial. Aquest programa correspon a una màquina d'estats finits (FSM), és a dir, un graf dirigit format per nodes (o vèrtexs) i arestes. A cada node s'associa un conjunt de proposicions atòmiques, que normalment indiquen quins elements de memòria són un. Els nodes representen estats d'un sistema, les arestes representen possibles transicions que poden alterar l'estat, mentre que les proposicions atòmiques representen les propietats bàsiques que es mantenen en un punt d'execució.

Formalment, el problema es pot enunciar de la següent manera: donada una propietat desitjada, expressada com una fórmula lògica temporal $p$ , i una estructura $M$ amb estat inicial $s$ , decideix si $M,s\models p$ . Si $M$ és finit, com en el maquinari, la comprovació de models es redueix a una cerca de gràfics.

Comprovació de models simbòlics

En lloc d'enumerar els estats accessibles d'un en un, de vegades es pot recórrer l'espai d'estats de manera més eficient considerant un gran nombre d'estats en un sol pas. Quan aquest recorregut de l'espai d'estat es basa en representacions d'un conjunt d'estats i relacions de transició com a fórmules lògiques, diagrames de decisió binaris (BDD) o altres estructures de dades relacionades, el mètode de verificació de models és simbòlic.

Històricament, els primers mètodes simbòlics utilitzaven BDD. Després de l'èxit de la satisfacció proposicional en la resolució del problema de planificació en intel·ligència artificial (vegeu satplan) l'any 1996, el mateix enfocament es va generalitzar a la verificació de models per a la lògica temporal lineal (LTL): el problema de planificació correspon a la verificació de models de propietats de seguretat. Aquest mètode es coneix com a verificació de models acotats.^[5] L'èxit dels solucionadors de satisfacció booleans en la comprovació de models acotats va portar a l'ús generalitzat de solucionadors de satisfacció en la comprovació simbòlica de models.^[6]

Exemple

Un exemple d'aquest requisit del sistema: entre el moment en què es crida a un ascensor en un pis i el moment en què obre les portes en aquest pis, l'ascensor pot arribar a aquest pis com a màxim dues vegades. Els autors de "Patrons en l'especificació de propietats per a la verificació d'estats finits" tradueixen aquest requisit a la fórmula LTL següent:

${\begin{aligned}\Box {\Big (}({\texttt {call}}\land \Diamond {\texttt {open}})\to &{\big (}(\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor ((\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (\lnot {\texttt {atfloor}}~{\mathcal {U}}~{\texttt {open}})))))))){\big )}{\Big )}\end{aligned}}$

Aquí, $\Box$ s'ha de llegir com "sempre", $\Diamond$ com "finalment", ${\mathcal {U}}$ com "fins" i els altres símbols són símbols lògics estàndard, $\lor$ per "o", $\land$ per "i" i $\lnot$ per "no".

Tècniques

Les eines de verificació de models s'enfronten a una explosió combinatòria de l'espai d'estats, comunament coneguda com el problema de l'explosió d'estats, que s'ha d'abordar per resoldre la majoria dels problemes del món real. Hi ha diversos enfocaments per combatre aquest problema.

Els algorismes simbòlics eviten mai construir explícitament el gràfic per al FSM; en canvi, representen el gràfic implícitament utilitzant una fórmula en lògica proposicional quantificada. L'ús de diagrames de decisió binaris (BDD) es va popularitzar pel treball de Ken McMillan, així com d'Olivier Coudert i Jean-Christophe Madre, ^[7] i el desenvolupament de biblioteques de manipulació de BDD de codi obert com CUDD.^[8] i Buddy.^[9]
Els algorismes de verificació de models limitats desenrotllen el FSM per a un nombre fix de passos, $k$ , i comproveu si es pot produir una infracció de la propietat a $k$ o menys passos. Normalment, això implica codificar el model restringit com a instància de SAT. El procés es pot repetir amb valors cada cop més grans de $k$ fins que s'hagin descartat totes les possibles infraccions (cf. Aprofundiment iteratiu de cerca en profunditat).
L'abstracció intenta demostrar les propietats d'un sistema simplificant-lo primer. El sistema simplificat normalment no satisfà exactament les mateixes propietats que l'original de manera que pot ser necessari un procés de perfeccionament. En general, cal que l'abstracció sigui sòlida (les propietats demostrades en l'abstracció són certes del sistema original); tanmateix, de vegades l'abstracció no és completa (no totes les propietats veritables del sistema original són certes de l'abstracció). Un exemple d'abstracció és ignorar els valors de les variables no booleanes i considerar només les variables booleanes i el flux de control del programa; aquesta abstracció, encara que pugui semblar tosca, pot, de fet, ser suficient per demostrar, per exemple, propietats d'exclusió mútua.
El refinament de l'abstracció guiada per contraexemple (CEGAR) comença a comprovar amb una abstracció grossa (és a dir, imprecisa) i la perfecciona iterativament. Quan es troba una violació (és a dir, contraexemple), l'eina l'analitza per determinar-ne la viabilitat (és a dir, la violació és genuïna o és el resultat d'una abstracció incompleta?). Si la infracció és factible, s'informa a l'usuari. Si no és així, s'utilitza la prova de inviabilitat per refinar l'abstracció i es torna a començar la comprovació.

Les eines de verificació de models es van desenvolupar inicialment per raonar sobre la correcció lògica dels sistemes d'estats discrets, però des d'aleshores s'han estès per fer front a les formes limitades i en temps real de sistemes híbrids.

Referències

↑ Lam K., William. «Chapter 1.1: What Is Design Verification?». A: Hardware Design Verification: Simulation and Formal Method-Based Approaches (en anglès), 2005.
↑ «Amir Pnueli - A.M. Turing Award Laureate» (en anglès).
↑ «Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology» (en anglès). Arxivat de l'original el 2008-12-28. [Consulta: 6 gener 2009].
↑ Grobelna, Iwona. «Model Checking of UML Activity Diagrams in Logic Controllers Design». A: Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland (en anglès). 286, 2014, p. 233–242 (Advances in Intelligent Systems and Computing). DOI 10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.
↑ Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. Formal Methods in System Design, 19, 2001, pàg. 7–34. DOI: 10.1023/A:1011276507260.
↑ Vizel, Y.; Weissenbacher, G.; Malik, S. Proceedings of the IEEE, 103, 11, 2015, pàg. 2021–2035. DOI: 10.1109/JPROC.2015.2455034.
↑ Coudert, O. «A unified framework for the formal verification of sequential circuits». A: 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers (en anglès). IEEE Comput. Soc. Press, 1990, p. 126–129. DOI 10.1109/ICCAD.1990.129859. ISBN 978-0-8186-2055-3.
↑ «CUDD: CU Decision Diagram Package» (en anglès).
↑ «BuDDy – A Binary Decision Diagram Package» (en anglès).

[1] Lam K., William. «Chapter 1.1: What Is Design Verification?». A: Hardware Design Verification: Simulation and Formal Method-Based Approaches (en anglès), 2005.

[2] «Amir Pnueli - A.M. Turing Award Laureate» (en anglès).

[3] «Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology» (en anglès). Arxivat de l'original el 2008-12-28. [Consulta: 6 gener 2009].

[4] Grobelna, Iwona. «Model Checking of UML Activity Diagrams in Logic Controllers Design». A: Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland (en anglès). 286, 2014, p. 233–242 (Advances in Intelligent Systems and Computing). DOI 10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.

[5] Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. Formal Methods in System Design, 19, 2001, pàg. 7–34. DOI: 10.1023/A:1011276507260.

[6] Vizel, Y.; Weissenbacher, G.; Malik, S. Proceedings of the IEEE, 103, 11, 2015, pàg. 2021–2035. DOI: 10.1109/JPROC.2015.2455034.

[7] Coudert, O. «A unified framework for the formal verification of sequential circuits». A: 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers (en anglès). IEEE Comput. Soc. Press, 1990, p. 126–129. DOI 10.1109/ICCAD.1990.129859. ISBN 978-0-8186-2055-3.

[8] «CUDD: CU Decision Diagram Package» (en anglès).

[9] «BuDDy – A Binary Decision Diagram Package» (en anglès).

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]