Egiaztapen formala (informatika)

Egiaztapen formala (hardware eta softwareen sistemei dagokionez), algoritmo jakin bat espezifikazio formal batekiko zuzena dela frogatzean datza, horretarako matematikak eskaintzen dituen metodo formalak medio direlarik.^[1]

Algoritmo hauen egiaztapena gauzatzako, dagokion sistemaren (hardware edo softwarea, kasuak kasu) eredu matematiko abstraktu batean oinarritzen den froga formal bat eman behar da. Hauek dira sistemen eredutzat erabiltzen diren eredu matematiko batzuk: egoera makina finituak, etiketadun igarotze sistemak, Petriren sareak, bektore batuketarako sistemak, automata denborizatuak, automata hibridoak, prozesuen aljebra, semantika operazionala eta Hoareren logika.^[2]

Garrantzia softwarean

Egiaztapen formalak softwarean, programa bat espezifikazio formal batek dioena betetzen duela frogatzea du helburu. Software egiaztapen formalaren esparruan hurrengo eremuak nabarmentzen dira: egiaztapen deduktiboa, interpretazio abstraktua eta mota sistemak. Menpeko programazio "motatua" etorkizunean interesgarri izan daitekeen egiaztapen planteamendu bat da non programa bateko funtzioek itzultzen duten balioen motek funtzioaren espezifikazioa (edo haren parte) adierazten dute.

Beste planteamendu indartsu bat softwarearen egiaztapena gauzatzeko programen eratorpenean datza. Paradigma honek espezifikazio batetik kode eraginkorra sortzea ahalbidetzen du espezifikazioaren zuzentasuna mantentzen duten pauso batzuk medio direlarik.

Softwarearen egiaztapenerako teknikak honela sailkatzen dira betetzen dituzten ezaugarrien arabera:

Sendoak: Egiaztatutako propietateak logikoki ondoriozta daitezke egiaztatutakoaren esanahi semantikotik. Honelako teknikak erabiltzerakoan aukera guztiak aztertu behar dira edozein emaitza lortzeko.
Ez-Sendoak: Ez dago bermatuta egiaztatutako propietatea logikoki ondoriozta daitekeenik esanahi semantikotik. Teknika ez-sendoek aukeren azpimultzo bat baino ez dute kontuan hartzen zuzentasuna ondorioztatzeko.
Erabakigarria: Teknikaren inplementazio algoritmikoa bermatuta badago erantzun batekin bukatzea.
Erabakiezina: Teknikaren inplementazio algoritmikoak agian (sarrera parametroen arabera) ez du inoiz konputazioa bukatuko, eta beraz ez da erantzun bat lortuko.

Egiaztapena eta balioespena

Egiaztapena, produktu bat bete beharreko helbururako egokia denentz aztertzerakoan alderdi bat da. Balioespena egiaztapenaren alderdi osagarria da.

Egiaztapen prozesua, egitura eta jokabidearekiko azterketez osatua dago. Adibidez software produktu batean egituraren azterketa iturburu-kodearen azterketaren analogoa izango litzateke eta kodearen exekuzioa proba-kasu jakin batzuk probatuz jokabidearekiko azterketaren analogoa. Sarritan balioespena dinamikoki baino ezin daiteke egin, produktua erabilera tipiko eta atipikoetan probatuz halaber.

Balioespena: Produktuaren espezifikazioa erabiltzailearen beharretara egokitzen da?
Egiaztapena: Produktuak betetzen al du ezarritako espezifikazioa?

Programen egiaztapen formala

Programen zuzentasuna

Programa baten zuzentasuna , programaren ustezko portaera ezartzen duen deskribapen formal batekiko erabakitzen da. Bi zuzentasun mota bereizten dira:

Zuzentasun partziala: P programa bat (φ,ψ) espezifikazio batekiko (non 'φ' aurrebaldintza eta ψ' postbaldintza den) partzialki zuzena da baldin eta soilik baldin φ betetzen duen konputazio-egoeran hasita(hau da, programaren aldagaien balioak φ ezartzen dituen irizpideak betetzen dituzte) P programaren exekuzioa burutuz ψ betetzen duen konputazio-egoeran bukatzen bada. Partzialki zuzena izateak ez du bermatzen, ordea, konputazioa inoiz bukatuko denik, bakarrik bermatzen du bukatzekotan ψ egoeran bukatuko dela.

Zuzentasun osoa: P programa bat (φ,ψ) espezifikazio batekiko guztiz zuzena izango da, partzialki zuzena izateaz gain φ aurrebaldintza betetzen duen konputazio-egoera batean hasita programaren exekuzioa bukatzen bada.

Hoareren sistema formala

Hoare-ren sistema formala, programei buruzko zuzentasun partzialeko baieztapenak frogatzeko sistema formal bat da. Hoare-ren sisteman programa edo agindu-segida bat espezifikazio batekiko partzialki zuzena dela adierazteko {φ}P{ψ} motako adierazpen bat erabiltzen da, mota honetako baieztapenak Hoareren hirukote izena hartzen dute eta hauek frogatzean datza Hoareren kalkulua.

Hoareren sistemak Hoareren hirukoteak frogatzen laguntzen badu ere ezin dezake baieztapen bat faltsua dela frogatu, kasu honetan kontraadibide bat aurkitu daiteke faltsutasuna frogatzeko. {φ}P{ψ} hirukote baten kontraadibidea konputazio-egoera (aldagaien balio konkretu batzuk) jakin bat izango da non φ aurrebaldintza betetzen den P-ren exekuzio aurretik eta honen exekuzioaren ondoren ψ betetzen ez den.

Frogapena gauzatzeko sistema honek hainbat axioma eta inferentzi erregela eskaintzen ditu agindu mota ezberdinei dagozkien Hoareren hirukoteak frogatzeko. Adibidez:

Esleipenaren axioma: Esleipen edo asignazio motako aginduak frogatzeko.
Ondorioaren erregela: Aurrebaldintza gogorregiak edo postbaldintza ahulegiak dituzten hirukoteak tratatzeko.
Konposaketaren erregela: Ondoz-ondoko agindu-segidei dagozkien hirukoteak frogatzeko.
Baldintzaren erregela: Baldintzazko aginduak frogatzeko (If-else...-end if motako aginduak).
While-aren erregela: while motako agindu iteratiboak frogatzeko.

Programen zuzenketa automatikoa

Programen zuzenketa automatikoa software erroreak zuzentzean datza inolako giza laguntza gabe (edo oso laguntza mugatuarekin). Programen zuzenketa orakulu bat erreferentzia gisa izanik egiten da, orakulu honek programatik espero den funtzionalitatea biltzen duelarik. Behin zuzenketa ekoiztu denean orakulua erabiliko da hau balioesteko. Programaren zuzenketa automatikoan hainbat teknika erabiltzen dira, adibidez programazio genetikoa^[3] non konputazio ebolutiboaren bidez, programazio akats baten konponbide posibleak ekoiztu eta probatu egiten dira.

Programen arazketan, egiaztapen formalak eta programa sintesiak eskaintzen dituzten teknikak konbinatzen dira. Egiaztapen formaletik, esaterako, akatsak aurkitzeko teknikak erabiltzen dira programa batean akatsak sor ditzaketen kode lerroak aztertzeko. Kode lerroak akastunak balira, sintesi moduluak arduratuko ziren orakuluak adierazten duen funtzionalitatera egokitzen diren kode lerroak ekoizteaz eta lerro akastunak hauengatik ordezkatzeaz.

Programa zuzenketa sistemak bakarrik arduratu ohi dira akatsen multzo konkretu batzuetako akatsak zuzentzeaz, zuzenketa denbora murriztea helburu delarik.

Erabilera industrian

Diseinuaren konplexutasunaren hazkundea dela eta hardware industrian egiaztapen formalerako dauden teknikak inoiz baino garrantzitsuagoak dira.^[4] ^[5] Gaur egun hardware enpresa handi guztiek egiaztapen formala erabiltzen dute^[6], software industriari dagokionez ordea, erabilera ez da hain hedatua. Hardwarearen industrian, egiaztapen formalaren beharraren arrazoia da diseinu mailako errore batek dakartzan ondorio komertzial latzak ekiditeko nahia. Gainera, hardwarearen konplexutasuna handitzen den heinean gero eta zailagoa da produktu baten zuzentasuna aztertzeko proba-kasu multzo batekiko simulazioak egitea, eta egiaztapen formala, aldiz, beste teknika batzuekin alderatuta errazagoa eta emankorragoa da.^[7]

Erreferentziak

↑ Sanghavi, Alok (21 May 2010). "What is formal verification?". EE Times_Asia.
↑ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013
↑ Le Goues, ThanhVu Nguyen; Forrest, Weimer (2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Trans. Software Eng. », 1, 38, 2012, 54-72.
↑ Harrison, J. (2003). "Formal verification at Intel": 45–54. doi:10.1109/LICS.2003.1210044.
↑ Formal verification of a real-time hardware design. Portal.acm.org (1983-06-27). Retrieved on April 30, 2011.
↑ "Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015.
↑ "Formal Verification in Industry" (PDF). Retrieved September 20, 2012.

Bibliografia

Javier Alvez Gimenez, Xabier arregi Iparragirre, Jose Gaintzarain Ibarmia, Paqui Lucio Carrasco, Montse Maritxalar Anglada. Programen espezifikazio, egiaztapen eta eratorpen formala. Udako Euskal Unibertsitatea. 2016. ISBN:978-84-8438-590-5

Kanpo estekak

Datuak: Q173326

[1] Sanghavi, Alok (21 May 2010). "What is formal verification?". EE Times_Asia.

[2] Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013

[3] Le Goues, ThanhVu Nguyen; Forrest, Weimer (2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Trans. Software Eng. », 1, 38, 2012, 54-72.

[4] Harrison, J. (2003). "Formal verification at Intel": 45–54. doi:10.1109/LICS.2003.1210044.

[5] Formal verification of a real-time hardware design. Portal.acm.org (1983-06-27). Retrieved on April 30, 2011.

[6] "Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015.

[7] "Formal Verification in Industry" (PDF). Retrieved September 20, 2012.

[1]

[2]

[3]

[4]

[5]

[6]

[7]