Formális programellenőrzés a gyakorlatban

Megpróbálok tömör választ adni néhány kérdésére.Kérjük, vegye figyelembe, hogy ez nem kizárólag az én kutatási területem, ezért egyes információim elavultak / helytelenek lehetnek.

1. Sok olyan eszköz van, amelyet kifejezetten a tulajdonságok hivatalos igazolására terveztek Java és C ++.

   Mindazonáltal el kell végeznem egy kis eltérést: mit jelent a program helyességének bizonyítása? A Java típusú ellenőrző bizonyítja a Java program formális tulajdonságát, nevezetesen, hogy bizonyos hibák, például egy float és egy int hozzáadása soha nem tudnak soha előfordul! Úgy gondolom, hogy sokkal erősebb tulajdonságok érdekelnek, nevezetesen az, hogy a program soha nem léphet be nem kívánt állapotba, vagy hogy egy bizonyos függvény kimenete megfelel egy bizonyos matematikai specifikációnak. Röviden, széles skálán mozoghat, hogy mit is jelenthet a “program helyes igazolása”, az egyszerű biztonsági tulajdonságoktól a teljes bizonyítékig, hogy a program teljesíti a részletes specifikációt.

   Most azt fogom feltételezni, hogy érdekel, hogy bizonyítsd a programod erős tulajdonságait. Ha érdekelnek a biztonsági tulajdonságok (a programod nem elérhet egy bizonyos állapotot), akkor általában úgy tűnik, hogy a legjobb megközelítés a modellellenőrzés . Ha azonban teljes körűen meg szeretné adni a Java program viselkedését, akkor a legjobb megoldás, ha az adott nyelvhez egy specifikációs nyelvet használ, például JML . Vannak ilyen nyelvek a C programok viselkedésének meghatározásához, például ACSL , de erről nem tudok C ++.

2. Miután megadta a specifikációkat, be kell bizonyítania, hogy a program megfelel az adott specifikációnak.

   Ehhez szüksége van egy eszközre, amely rendelkezik mindkettő formális megértése specifikációját és nyelvének operatív szemantikáját (Java vagy C ++) annak érdekében, hogy kifejezze a megfelelőségi tételt , nevezetesen, hogy a végrehajtás A program megfelel a specifikációnak.

   Ennek az eszköznek lehetővé kell tennie a tétel bizonyítékának megfogalmazását vagy előállítását is. Most mindkét feladat (megadás és igazolás) meglehetősen nehéz, ezért gyakran kettéválnak:

   • Az egyik eszköz, amely elemzi a kódot, a specifikáció és létrehozza a megfelelőségi tételt. Mint Frank említette, a Krakatoa példa egy ilyen eszközre.

   • Az egyik eszköz, amely a tételt bizonyítja ( s) automatikusan vagy interaktív módon. A Coq ilyen módon lép kölcsönhatásba a Krakatoa-val, és vannak olyan hatékony automatizált eszközök, mint a Z3 , amelyek szintén használhatók.

   Egy (kisebb) pont: vannak olyan tételek, amelyeket túl nehéz megvizsgálni az automatizált módszerekkel, és az automatikus tétel-bizonyítókról ismert, hogy időnként vannak hibabejelentési hibák, amelyek kevésbé megbízhatóvá teszik őket. Ez egy olyan terület, ahol a Coq ragyog az összehasonlításhoz (de ez nem automatikus!).

3. Ha Ocaml kódot akar generálni, akkor először mindenképpen Coq-ban (Gallina) írjon, majd vonja ki a kódot. A Coq azonban szörnyű a C ++ vagy a Java generálásában, ha ez még lehetséges.

4. A fenti eszközök képesek kezelni a szálak és a teljesítmény problémáit? Valószínűleg nem, a teljesítmény- és menetproblémákat a legjobban speciálisan tervezett eszközök kezelik, mivel ezek különösen nehéz problémák. Nem vagyok biztos benne, hogy vannak-e itt ajánlandó eszközeim, bár Martin Hofmann “s PolyNI projektje érdekesnek tűnik.

Összegzésképpen: A “valós világ” Java és C ++ programjainak hivatalos ellenőrzése nagy és fejlett terület, és a Coq alkalmas ennek a feladatnak a részeire. Magas szintű áttekintést talál például itt .

Megjegyzések

• Köszönöm ezt a bejegyzést és a hozzáadott referenciákat. IMHO, a szoftvermérnökök célja, hogy képesek legyenek gyorsan felszabadítani azokat a rendszereket, amelyek 1) mindig megfelelő eredményt nyújtanak, 2) soha nem fognak kudarcot vallani. Láthattam itt egy regressziós problémát, ahol érdemes bizonyítania, hogy a specifikáció maga ” hibamentes ” 🙂 mint egy ” egy nyelv igaz felvetését ” egy metanyelvvel megpróbálni definiálni, majd ehhez másik metanyelvre van szükség, majd egy másikra egy …
• A probléma az, hogy amit a ” felhasználó ” szeretne, azt általában nem fejezik ki formális formában. nyelv! A kérdésre általában nincs formális válasz: ” megfelel-e ez a hivatalos specifikáció az informális elképzelésemnek? “. ‘ lehetséges tesztelni egy hivatalos specifikációt és bebizonyítani, hogy bizonyos matematikai tulajdonságokkal rendelkezik, de végső soron össze kell kapcsolnia a matematikát a való világgal, ami nem formális folyamat.
• Természetesen igen – mindig rájöttem, hogy a formális módszerek csak egy jól meghatározott pontról indulhatnak ki.Ha ez a specifikáció megfelel a valós életben élők tudatos / tudattalan / felfedezetlen igényeinek, akkor ez egy másik probléma, amely formális módszerekkel nem kezelhető (de a mérnökök számára mindenképpen probléma).
• A tétel definíció szerint egy bizonyított javaslat. Tehát valószínűleg nem azt akarja mondani, hogy ” bebizonyítsa a ” tételt.
• Úgy tűnik, hogy a Wikipédia @ nbro egyetért veled. A Mathworld azonban egy tételt olyan tételként határoz meg, amely ” igazolható elfogadott matematikai műveletekkel igazolható “. Ebben az esetben a tételek igazolása nem csak lehetséges, hanem szükséges is annak igazolásához! 🙂 (ez természetesen egy ellentámadás)

Három figyelemre méltó alkalmazást szeretnék megemlíteni formális módszerek / formális ellenőrzési eszközök az iparban vagy a nem triviális valós rendszerek. Ne feledje, hogy kevés tapasztalatom van ebben a témában, és csak tanulmányokból tanulom őket.

1. A nyílt forráskódú eszköz Java Pathfinder (röviden JPF) , amelyet a NASA adott ki 2005-ben , a futtatható Java bytecode programok ellenőrzésére szolgáló rendszer (lásd: Java Pathfinder @ wiki ). Ezt alkalmazták a K9 Rover végrehajtó szoftverének következetlenségeinek felderítésére a NASA Ames-ben.

2. iv

Hivatalos a program specifikációja (többé-kevésbé) egy másik programozási nyelven írt program. Ennek eredményeként a specifikáció minden bizonnyal tartalmazni fogja a saját hibáit is.

A hivatalos ellenőrzés előnye, hogy mivel a program és a specifikáció két külön megvalósítás, hibáik különbözőek lesznek. De nem mindig: a hibák egyik gyakori forrása, figyelmen kívül hagyott esetek gyakran meg fognak egyezni. Így a hivatalos ellenőrzés nem csodaszer: még mindig hiányozhat a nem triviális számú hiba.

A hivatalos ellenőrzés hátránya, hogy a végrehajtás költségének kétszeresét, valószínűleg többet is kivethet (szükséged van rá) a hivatalos specifikáció szakembere, és használnia kell a hozzá tartozó többé-kevésbé kísérleti eszközöket, amelyek nem lesznek olcsók.

Azt hiszem, teszt esetek és állványok felállítása futtatásukhoz automatikusan jobban felhasználná az idejét.

Megjegyzések

• A hivatalos ellenőrzés előnye az, hogy … . A hivatalos ellenőrzés második hátránya az, hogy … Ez zavarba ejtő.
• Úgy gondolom, hogy a specifikáció és az informális feladat közötti eltérés szoftverkövetelmény-elemzési kérdés, nem pedig programozási kérdés.

Néhány különböző kérdést tesz fel. Egyetértek azzal, hogy az ipari / kereskedelmi alkalmazások hivatalos ellenőrzési módszerei nem annyira elterjedtek. rá kell jönni azonban arra, hogy a fordítókba sok “formális ellenőrzési” elv van beépítve a program helyességének megállapításához! Tehát bizonyos értelemben, ha modern fordítót használ, akkor a formális ellenőrzés során a legkorszerűbb dolgok nagy részét felhasználja.

Azt mondod: “Elegem van a tesztelésből”, de a hivatalos ellenőrzés valójában nem helyettesíti a tesztelést. bizonyos értelemben a tesztelés változata .

Megemlíti a Java-t.sok fejlett formális ellenőrzési módszer van beépítve a FindBugs nevű java ellenőrző programba, amelyek valóban nagy kódbázisokon futtathatók. Ne feledje, hogy mind a “hamis pozitív, mind a hamis negatívok” kiderülnek, és az eredményeket egy emberi fejlesztőnek kell felülvizsgálnia / elemeznie. De vegye figyelembe, még akkor is, ha ez nem valós funkcionális hibákat mutat be, általában olyan “antipatternákat” jelenít meg, amelyeket egyébként is el kell kerülni a kódban.

Az “ipari” kivételével többet nem említ az adott alkalmazásáról. . A formális ellenőrzés a gyakorlatban általában az adott alkalmazástól függ.

Úgy tűnik, hogy az EE-ben a formális ellenőrzési technikákat széles körben használják az áramkör helyességének igazolására, pl. a mikroprocesszor tervezésében.

Íme egy példa a formális ellenőrző eszközök felmérésére az EE mezőben, amelyet Lars Philipson készített.

Megjegyzések

• ‘ félrevezető azt mondani, hogy ” a a ” formális ellenőrzés ” alapelvek beépülnek a fordítókba a program helyességének meghatározásához ” Amire hivatkozol, az a statikus típusellenőrzés, amelyet néhány fordító végez, de az így ellenőrzött tulajdonságok meglehetősen egyszerűek, pl. kerülje a szám és a karakterlánc hozzáadását. Ez hasznos, de messze van attól, amit általában ” formális ellenőrzés ” értelmez.
• nem kifejezetten statikus típusellenőrzésre utalnak, bár ez az egyszerű / általános példa. Az széles körben elterjedt és fejlett imho fordító optimalizálási technikák nagyjából hasonlóak a hivatalos ellenőrzési elvekhez, mert fejlett technikákkal járnak az optimalizált programváltozatok egyenértékűségének meghatározására / bemutatására. ezért fontosnak tűnik elkerülni a ” mozgó célposztok ” kérdést itt, és nem feltételezni, hogy pusztán azért, mert egy fordító csinálja vagy építi fel a fordítóba, annak nem hivatalos ellenőrzése.
• egyetértett abban, hogy ez nem általános megegyezés. Az optimalizálási technikák nagyjából a program viselkedésének modelljét hozzák létre, például egy hurokból vagy alprogramból, és optimalizálják ezt a modellt, majd új, bizonyíthatóan ekvivalens kódot hoznak létre. így ezeknek az optimalizálásoknak egy része meglehetősen bonyolult a & kód átrendezésében, számomra hivatalos ellenőrzési elveket alkalmaznak. úgy tűnik, hogy a fordítóban számos más példa található a hivatalos ellenőrzési módszerekre … az eredeti kérdés sokféle kérdést tett fel, amint azt sokan megjegyezték, de nem próbálom megválaszolni az összes benne szereplő kérdést.
• a úgy tűnik, hogy vannak bizonyos formális ellenőrzési elvek, amelyeket a JRE, a java futásidejű motor is használ, pl. dinamikus optimalizálás stb.
• vagyis ” a álom a hivatalos igazolásról “, amelyet a filmus említett, imho kiméra absztrakció, és a pragmatikus / haszonelvű / realista ipar nagyrészt ilyennek ismeri el. A nagy kódbázisokról évtizedek óta ismert, hogy $ x $ hibákat / hibákat tartalmaznak egy $ y $ K-soronként, és ez soha nem fog változni, bármennyire is halad az elmélet / technológia, ez tény emberi természet. és valójában az ember által létrehozott matematikai tételek ugyanazokkal a tulajdonságokkal bírnak, bár ezt nem nagyon értékelik!

Talán hasznos lehet egy modellellenőrző.

http://alloytools.org/documentation.html Alloy egy modellellenőrző .

Szép bemutató, amely elmagyarázza a modellellenőrzés fogalmát az Alloy használatával: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Ugyanabban az eszközcsaládban szerepel a „tulajdonság-alapú tesztelés”, mindannyian megpróbálnak egy ellenpéldát találni a szoftvered adott specifikációs modelljéhez.