SPIN

Straipsnis iš Vikipedijos, laisvosios enciklopedijos.
Peršokti į: navigaciją, paiešką

SPIN (angl. Simple Promela Interpreter) - bendro pobūdžio priemonės, skirtos griežtai ir dažniausiai automatizuotai patikrinti, ar platinamos programinės įrangos modelis yra teisingas.

Istorija[taisyti | redaguoti kodą]

SPIN buvo parašyta Gerard J. Holzmann ir kitų Unix grupės asmenų dirbančių Kompiuterinių technologijų tyrimų centre "Bell Labs", 1980 m. pradžioje.

Nuo 1991 m. prieinama laisvai.

Nuo maždaug 1995 m. buvo rengiami metiniai SPIN seminarai vartotojams, mokslininkams, besidomintiems modelių tikrinimu.

2001 m. Kompiuterinės technikos asociacija apdovanojo SPIN savo programinės įrangos apdovanojimu.

Veikimas[taisyti | redaguoti kodą]

Tikrinamos sistemos aprašytos Promela (proceso Meta kalba), kuri palaiko asinchroninius algoritmus kaip ne deterministiniai automatai. Parametrai kurie yra tikrinami yra išreiškiamas pagal Linijinio laiko logikos formules (Linear Temporal Logic, LTL)), kurios yra neveiksmingos, o tada keičiami į Buchi automatus kaip dalis modelio patikrinimo algoritmo. Be modelio patikrinimo, SPIN taip pat gali veikti kaip simuliatorius, sekti vieną pasirinktą vygdymo kelią per sistemą ir pateikti užfiksuotus vykdymo rezultatus vartotojui.

Skirtingai nuo daugelio modelių tikrinimo sistemų, pati SPIN sistema iš tikrųjų neatlieka modelio tikrinimo, o tik sukuria C šaltinius modelių specifinių problemų tikrinimui. Šis metodas leidžia sutaupyti atminties ir didina našumą, o taip pat, leidžia tiesiogiai įterpti C kodo gabaliukus į modelį. SPIN taip pat siūlo daug galimybių toliau spartinti modelio patikros procesą ir saugoti atmintį, kaip antai:

  • ne pilnų užsakymų sumažinimas;
  • būsenos suspaudimas;
  • bitų būsenos maiša (vietoje to kad saugoti visą būseną, tik jų maišos kodas yra prisimenamas bitų lauke, tai sutaupo daug atminties, tačiau prarandamas detalumas);
  • silpnas teisingumo vykdymas.

Literat9ra[taisyti | redaguoti kodą]

Nuorodos[taisyti | redaguoti kodą]