Formální ověření programu v praxi

Pokusím se na vaše dotazy stručně odpovědět.Pamatujte, že to není výhradně moje oblast výzkumu, takže některé moje informace mohou být zastaralé / nesprávné.

1. Existuje mnoho nástrojů, které jsou speciálně navrženy k formálnímu prokázání vlastností Java a C ++.

   Zde však musím udělat malou odbočku: co to znamená prokázat správnost programu? Kontrola typu Java dokazuje formální vlastnost programu Java, konkrétně to, že určité chyby, jako například přidání float a int, nikdy nemohou nastat! Představuji si, že vás zajímají mnohem silnější vlastnosti, konkrétně to, že váš program nikdy nemůže přejít do nežádoucího stavu nebo že výstup určité funkce odpovídá určité matematické specifikaci. Stručně řečeno, existuje široká škála toho, co může znamenat „prokázání správnosti programu“, od jednoduchých vlastností zabezpečení až po úplný důkaz, že program splňuje podrobnou specifikaci.

   Nyní budu předpokládat, že máte zájem prokázat silné vlastnosti svých programů. Pokud vás zajímají vlastnosti zabezpečení (váš program nemůže dosáhnout určitého stavu), pak se obecně zdá, že nejlepší přístup je kontrola modelu . Pokud si však přejete plně specifikovat chování Java programu, nejlépe použijte specifikační jazyk pro tento jazyk, například JML . Existují takové jazyky ke specifikaci chování programů C, například ACSL , ale nevím o C ++.

2. Jakmile budete mít své specifikace, musíte prokázat, že program odpovídá této specifikaci.

   K tomu potřebujete nástroj, který má formální porozumění obou vaše specifikace a operační sémantika vašeho jazyka (Java nebo C ++) za účelem vyjádření věty přiměřenosti , konkrétně že provedení programu respektuje specifikaci.

   Tento nástroj by vám měl také umožnit formulovat nebo vygenerovat důkaz této věty. Nyní jsou oba tyto úkoly (upřesnění a prokázání) poměrně obtížné, takže se často dělí na dvě části:

   • Jeden nástroj, který analyzuje kód, specifikaci a generuje teorém přiměřenosti. Jak Frank zmínil, Krakatoa je příkladem takového nástroje.

   • Jeden nástroj, který teorém dokazuje ( s), automaticky nebo interaktivně. Coq interaguje s Krakatoa tímto způsobem a existují i některé výkonné automatizované nástroje, jako je Z3 , které lze také použít.

   Jeden (vedlejší) bod: existují některé věty, které jsou příliš obtížné na to, aby je bylo možné ověřit automatizovanými metodami, a je známo, že automatické ověřovače teorémů občas obsahují chyby zvuku, díky nimž jsou méně důvěryhodné. Toto je oblast, kde Coq svítí ve srovnání (ale není to automatické!).

3. Chcete-li vygenerovat kód Ocaml, určitě nejprve napište Coq (Gallina), poté extrahujte kód. Coq je však hrozný při generování C ++ nebo Javy, pokud je to vůbec možné.

4. Mohou výše uvedené nástroje zvládnout problémy s vlákny a výkonem? Pravděpodobně ne, problémy s výkonem a vlákny nejlépe zvládnou speciálně navržené nástroje, protože to jsou obzvláště těžké problémy. Nejsem si jistý, zda zde mohu doporučit nějaké nástroje, i když projekt Martina Hofmanna PolyNI se zdá zajímavý.

Závěrem: formální ověření „reálného světa“ programů Java a C ++ je velká a dobře vyvinutá oblast a Coq je vhodný pro části tohoto úkolu. Přehled na vysoké úrovni najdete například zde .

Komentáře

• Děkujeme za tento příspěvek a odkazy, které jste přidali. IMHO je cílem softwarových inženýrů být schopen rychle uvolnit systémy, které 1) vždy poskytnou správné výsledky, 2) nikdy nezklamou. Viděl jsem zde problém s regresí, kde možná budete chtít dokázat, že samotná specifikace je “ chyba zdarma “ 🙂 druh jako zkoušet definovat “ opravdovou nabídku jazyka “ s metajazykem, pak k tomu potřebovat další metajazyk, pak další jedna …
• Problém je v tom, že to, co uživatel “ chce „, obvykle není formálně vyjádřeno Jazyk! Formální odpověď na otázku zpravidla neexistuje: “ odpovídá tato formální specifikace mé neformální myšlence? „. ‚ je možné otestovat formální specifikaci a dokázat, že má určité matematické vlastnosti, ale nakonec musíte matematiku uvést do souvislosti se skutečným světem, což je neformální proces.
• Ano, samozřejmě – vždy jsem si uvědomil, že formální metody mohou vycházet pouze z dobře definovaného bodu.Pokud tato specifikace odpovídá nebo neodpovídá vědomým / nevědomým / neobjeveným potřebám uživatelů v reálném životě, je to další problém, který nelze řešit formálními metodami (ale určitě problém pro inženýry).
• Věta je podle definice prokázaný návrh. Pravděpodobně tedy nemáte na mysli “ dokázat teorém „.
• @nbro Wikipedia zřejmě souhlasí s tebou. Mathworld však definuje větu jako propozici, kterou “ lze prokázat jako pravdivou pomocí přijatých matematických operací „. V tomto případě je důkaz důkazů vět nejen možný, ale je také nezbytný k tomu, aby se jim tak říkalo! 🙂 (toto je samozřejmě kontroverze)

Chtěl bych zmínit tři pozoruhodné aplikace formálních metod / nástrojů formálního ověřování v průmyslu nebo netriviálních reálných systémech. Všimněte si, že s tímto tématem mám jen málo zkušeností a učím se je pouze při čtení článků.

1. Open-source nástroj Java Pathfinder (zkráceně JPF) vydaný NASA v roce 2005 je systém pro ověřování spustitelných programů byte bytecode Java (viz Java Pathfinder @ wiki ). Používá se k detekci nesrovnalostí ve výkonném softwaru pro K9 Rover v NASA Ames.

2. Tento článek: Použití kontroly modelu k nalezení závažných chyb systému souborů @ OSDI „04 ukazuje, jak používat kontrola modelu k nalezení závažných chyb v souborových systémech. Systém s názvem FiSC je aplikován na tři široce používané a silně testované souborové systémy: ext3, JFS a ReiserFS a bylo nalezeno 32 závažných chyb. Získal cenu za nejlepší papír.

3. Tento dokument: Jak Amazon Web Services používá formální metody @ CACM „15 popisuje, jak AWS aplikuje formální metody na její produkty jako S3, DynamoDB, EBS a Internal distribution lock manager. Zaměřuje se na Lamportův nástroj TLA + . Mimochodem, Lamport intenzivně používal svůj vlastní soubor nástrojů TLA. Často poskytuje (celkem) formální ověření v TLA algoritmů / vět, které sám navrhl (stejně jako spoluautoři) v přílohách příspěvků.

Formální ověření je nyní možné u programů napsaných v podmnožině jazyka C ++ navržených pro kritické z hlediska bezpečnosti vestavěné systémy. Viz http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt pro krátkou prezentaci a http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf pro celý článek.

Komentáře

• Díky za odkazy. Pro ochranu před rotací odkazů by byl užitečný alespoň stručný přehled jejich obsahu, zejména proto, že vaše odkazy vedou na firemní web: ty mají tendenci se pravidelně reorganizovat a zabíjet všechny odkazy na stránky.

Formální Specifikace programu je (více či méně) program napsaný v jiném programovacím jazyce. Výsledkem bude, že specifikace bude určitě obsahovat své vlastní chyby.

Výhodou formálního ověření je, že jelikož program a specifikace jsou dvě samostatné implementace, jejich chyby se budou lišit. Ale ne vždy: jeden společný zdroj chyb, přehlížené případy, se často budou shodovat. Formální ověření tedy není všelékem: stále mu může chybět netriviální počet chyb.

Nevýhodou formálního ověření je, že může uložit něco jako dvojnásobek nákladů na implementaci, pravděpodobně více (potřebujete více specialista na formální specifikaci a musíte použít víceméně experimentální nástroje, které jsou k dispozici; které nebudou levné).

Odhaduji nastavení testovacích případů a lešení pro jejich spuštění automaticky by lépe využilo váš čas.

Komentáře

• Výhodou formálního ověření je, že … . Druhou nevýhodou formálního ověření je, že … To je matoucí.
• Myslím si, že nesoulad mezi specifikací a neformálním úkolem je problém analýzy požadavků na software, nikoli problém programování.

Zeptáte se na několik různých otázek. Souhlasím, zdá se, že formální metody ověřování pro průmyslové / komerční aplikace nejsou tak běžné. je třeba si uvědomit, že do kompilátorů je zabudováno mnoho principů „formálního ověření“, které určují správnost programu! svým způsobem tedy, pokud používáte moderní překladač, používáte při formálním ověřování většinu z toho nejmodernějšího.

Říkáte „Už mě unavuje testování“, ale formální ověřování není ve skutečnosti náhradou za testování. svým způsobem je to variace na testování.

Zmínil jste Javu.Existuje mnoho pokročilých metod formálního ověřování zabudovaných do java ověřovacího programu s názvem FindBugs , které lze skutečně spustit přes velké databáze kódů. Všimněte si, že se objeví „falešné pozitivy i falešné negativy“ a výsledky je třeba zkontrolovat / analyzovat lidským vývojářem. Všimněte si však, že i když se nejedná o skutečné funkční vady, obvykle se objeví „antipattery“, kterým byste se v kódu měli i tak vyhnout.

O své konkrétní aplikaci se již nezmíníte, kromě „průmyslové“. . Formální ověřování v praxi obvykle závisí na konkrétní aplikaci.

Zdá se, že formální ověřovací techniky jsou v EE široce používány k prokázání správnosti obvodů, např. v designu mikroprocesoru.

Zde je příklad průzkumu formálních ověřovacích nástrojů v poli EE od Larse Philipsona .

Komentáře

• Je ‚ zavádějící říkat, že “ a Do kompilátorů je zabudováno mnoho “ formálních ověřovacích “ principů určujících správnost programu „. To, na co odkazujete, je statická kontrola typu, kterou provádějí někteří překladači, ale takto ověřené vlastnosti jsou poměrně jednoduché, např. vyhnout se přidání čísla a řetězce. To je užitečné, ale daleko od toho, co obvykle chápeme “ formálním ověřením „.
• ne odkazovat konkrétně na kontrolu statického typu, i když je to jeden jednoduchý / běžný příklad. Techniky optimalizace kompilátoru imho, které jsou velmi rozšířené a pokročilé, jsou zhruba podobné formálním principům ověřování, protože zahrnují pokročilé techniky k určení / zobrazení ekvivalence optimalizovaných variant programu. takže se zdá, že je důležité vyhnout se “ pohyblivým brankám “ problému a nepředpokládat to pouze proto, že to dělá kompilátor do kompilátoru, jeho ne formální ověření.
• souhlasil, že to není běžné porozumění. optimalizační techniky zhruba vytvářejí model chování programu, např. smyčky nebo podprogramu, a optimalizují tento model a poté generují nový kód, který je prokazatelně ekvivalentní. takže některé z těchto optimalizací jsou při přepracování kódu & poměrně sofistikované, využívají formální zásady ověřování. zdá se, že v kompilátoru existuje mnoho dalších příkladů formálních ověřovacích metod … původní otázka položila mnoho různých otázek, jak si mnozí všimli, a já se nepokouším odpovědět na všechny otázky v nich obsažené.

způsob, jakým se zdají existovat některé formální zásady ověřování používané také v prostředí JRE, java runtime engine, např. dynamická optimalizace atd …

• to je “ the sen o formálním ověření „, o kterém hovoří filmus výše, je to chimérická abstrakce a pragmatický / užitkový / realistický průmysl to jako takový velmi uznává. o velkých kódových základnách je již po celá desetiletí známo, že mají neodmyslitelně chyby / defekty $ x $ na $ y $ K-řádky kódu, a to se nikdy nezmění bez ohledu na to, jak bude teorie / technologie postupovat, je to fakt lidská příroda. a ve skutečnosti člověkem vytvořené matematické věty mají stejné vlastnosti, i když to není příliš oceňováno!

Možná by mohla být užitečná kontrola modelu.

http://alloytools.org/documentation.html Alloy je kontrola modelu .

Pěkná prezentace vysvětlující koncept kontroly modelu pomocí Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Ve stejné skupině nástrojů přichází „testování založené na vlastnostech“, všechny se snaží najít protiklad pro daný model specifikace vašeho softwaru.