Wikiproiektu:EHU-Wikipedia 2017/Probalekua/Proba orria2
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 sitemaren (hardware edo softwarea, kasuak kasu) eredu matematiko abstraktu batean oinarritzen den froga formal bat eman behar da. Hauek dira sitemen eredutzat erabiltzen diren eredu matematiko batzuk: egoera makina finituak, etiketadun igarotze sistemak, Petriren sareak, bektore batuketarako sistemak, automata denborizatuak, automata hibridoak, prozesuen aljebra, semantika operazioanla eta Hoareren logika.[2]
Garrantzia softwarean[aldatu iturburu kodea]
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 motak funtzioaren espezifikazioa (edo haren parte) adierazten du.
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 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 bukatuko, eta beraz ez da erantzun bat lortuko.
Egiaztapena eta balioespena[aldatu iturburu kodea]
Egiaztapena produktu bat bete beharreko helbururako egokia denentz aztertzerakoan alderdi bat da. Balioespena egiaztapenaren alderdi osagarria da.
Egiaztapen prozesua, egitura eta jokabidearekiko azterketetaz 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 egiaztapena?