Formalna weryfikacja programu w praktyce

Spróbuję udzielić zwięzłej odpowiedzi na niektóre z Twoich pytań.Pamiętaj, że nie jest to ściśle moja dziedzina badań, więc niektóre z moich informacji mogą być nieaktualne / nieprawidłowe.

1. Istnieje wiele narzędzi zaprojektowanych specjalnie do formalnego potwierdzania właściwości języka Java i C ++.

   Jednak muszę tutaj zrobić małą dygresję: co to znaczy udowodnić poprawność programu? Narzędzie do sprawdzania typów w języku Java udowadnia formalną właściwość programu Java, a mianowicie, że niektóre błędy, takie jak dodanie float i int, nigdy nie mogą pojawić się! Wyobrażam sobie, że jesteś zainteresowany znacznie silniejszymi właściwościami, a mianowicie tym, że twój program nigdy nie może wejść w niepożądany stan lub że wyjście określonej funkcji jest zgodne z pewną specyfikacją matematyczną. Krótko mówiąc, istnieje szeroki zakres tego, co może oznaczać „udowodnienie poprawności programu”, od prostych właściwości bezpieczeństwa do pełnego dowodu, że program spełnia szczegółową specyfikację.

   Teraz zamierzam założyć, że chcesz udowodnić silne właściwości swoich programów. Jeśli interesują Cię właściwości bezpieczeństwa (Twój program nie może nie osiągnąć określonego stanu), to ogólnie wydaje się, że najlepszym podejściem jest sprawdzanie modelu . Jeśli jednak chcesz w pełni określić zachowanie programu Java, najlepiej jest użyć języka specyfikacji dla tego języka, na przykład JML . Istnieją takie języki do określania zachowania programów w C, na przykład ACSL , ale nie wiem C ++.

2. Gdy masz już swoje specyfikacje, musisz udowodnić, że program jest zgodny z tą specyfikacją.

   Do tego potrzebujesz narzędzia, które ma formalne zrozumienie obu specyfikację i semantykę operacyjną Twojego języka (Java lub C ++) w celu wyrażenia twierdzenia o adekwatności , a mianowicie, że wykonanie programu przestrzega specyfikacji.

   To narzędzie powinno również pozwolić na sformułowanie lub wygenerowanie dowodu tego twierdzenia. Teraz oba te zadania (określenie i udowodnienie) są dość trudne, więc często dzieli się je na dwie części:

   • Jedno narzędzie, które analizuje kod, specyfikację i generuje twierdzenie o adekwatności. Jak wspomniał Frank, Krakatoa jest przykładem takiego narzędzia.

   • Jedno narzędzie, które udowadnia twierdzenie ( s), automatycznie lub interaktywnie. Coq współdziała z Krakatoa w ten sposób i istnieje kilka potężnych zautomatyzowanych narzędzi, takich jak Z3 , których można również użyć.

   Jedna (drobna) uwaga: istnieją twierdzenia, które są zbyt trudne do udowodnienia metodami automatycznymi, a wiadomo, że automatyczne dowódcy twierdzeń czasami zawierają błędy poprawności, które czynią je mniej godnymi zaufania. Jest to obszar, w którym Coq świeci w porównaniu (ale nie jest to automatyczne!).

3. Jeśli chcesz wygenerować kod Ocaml, zdecydowanie napisz najpierw w Coq (Gallina), następnie wyodrębnij kod. Jednak Coq nie radzi sobie z generowaniem C ++ lub Javy, jeśli jest to w ogóle możliwe.

4. Czy powyższe narzędzia radzą sobie z problemami z wątkami i wydajnością? Prawdopodobnie nie, problemy z wydajnością i gwintowaniem najlepiej rozwiązywać za pomocą specjalnie zaprojektowanych narzędzi, ponieważ są to szczególnie trudne problemy. Nie jestem pewien, czy mam tu jakieś narzędzia do polecania, chociaż projekt PolyNI Martina Hofmanna wydaje się interesujący.

Podsumowując: formalna weryfikacja „rzeczywistych” programów Java i C ++ to duża i dobrze rozwinięta dziedzina, a Coq nadaje się do części tego zadania. Ogólne omówienie można znaleźć na przykład tutaj .

Komentarze

• Dzięki za ten post i dodane przez Ciebie referencje. IMHO, celem inżynierów oprogramowania jest możliwość szybkiego wydawania systemów, które 1) zawsze będą dostarczać poprawne wyniki, 2) nigdy nie zawiodą. Widziałem tutaj problem z regresją, gdzie możesz chcieć udowodnić, że sama specyfikacja jest ” pozbawiona błędów ” 🙂 na przykład próbując zdefiniować ” prawdziwą propozycję języka ” za pomocą metajęzyka, a potem potrzebować do tego innego metajęzyka, a potem innego jeden …
• Problem polega na tym, że to, czego użytkownik ” chce „, zwykle nie jest wyrażone w formie formalnej język! Generalnie nie ma formalnej odpowiedzi na pytanie: ” czy ta formalna specyfikacja jest zgodna z moim nieformalnym pomysłem? „. ' można przetestować formalną specyfikację i udowodnić, że ma ona pewne właściwości matematyczne, ale ostatecznie trzeba odnieść matematykę do świata rzeczywistego, co jest procesem nieformalnym.
• Tak, oczywiście – zawsze zdawałem sobie sprawę, że metody formalne mogą zaczynać się tylko od dobrze zdefiniowanego punktu.Jeśli ta specyfikacja jest zgodna lub nie ze świadomymi / nieświadomymi / nieodkrytymi potrzebami rzeczywistych użytkowników, to kolejny problem, którego nie można rozwiązać za pomocą metod formalnych (ale z pewnością problem dla inżynierów).
• Twierdzenie jest z definicji sprawdzona propozycja. Więc prawdopodobnie nie chcesz ” udowodnić twierdzenie „.
• @nbro Wikipedia wydaje się zgadzać z Tobą. Mathworld definiuje jednak twierdzenie jako twierdzenie, które ” można wykazać za pomocą akceptowanych operacji matematycznych „. W takim przypadku przedstawienie dowodów twierdzeń jest nie tylko możliwe, ale konieczne, aby uzasadnić ich nazywanie! 🙂 (jest to oczywiście kontrowersja)

Chciałbym wspomnieć o trzech niezwykłych zastosowaniach metod formalnych / narzędzi weryfikacji formalnej w przemyśle lub nietrywialnych rzeczywistych systemach. Zauważ, że mam niewielkie doświadczenie w tym temacie i uczę się ich tylko z artykułów.

1. Narzędzie open source Java Pathfinder (w skrócie JPF) wydany przez NASA w 2005 r. to system weryfikacji wykonywalnych programów kodu bajtowego Javy (patrz Java Pathfinder @ wiki ). Został użyty do wykrycia niespójności w oprogramowaniu wykonawczym dla łazika K9 w NASA Ames.

2. Ten artykuł: Używanie sprawdzania modelu do znajdowania poważnych błędów systemu plików @ OSDI „04 pokazuje, jak używać sprawdzanie modeli w celu znalezienia poważnych błędów w systemach plików. System o nazwie FiSC jest stosowany w trzech powszechnie używanych, mocno przetestowanych systemach plików: ext3, JFS i ReiserFS, i znaleziono 32 poważne błędy. Zdobył on nagrodę Best Paper Award.

3. Ten artykuł: Jak Amazon Web Services wykorzystuje formalne metody @ CACM „15 opisuje, jak AWS stosuje formalne metody do jego produkty, takie jak S3, DynamoDB, EBS i Internal Distributed Lock Manager. Koncentruje się na narzędziu Lamporta TLA + . Nawiasem mówiąc, Lamport intensywnie korzystał z własnego zestawu narzędzi TLA. Często przeprowadza (całkiem pełną) formalną weryfikację w TLA algorytmów / twierdzeń zaproponowanych przez niego (a także współautorów) w załącznikach do artykułów.

Formalna specyfikacja programu to (mniej więcej) program napisany w innym języku programowania. W rezultacie specyfikacja z pewnością będzie zawierała własne błędy.

Zaletą weryfikacji formalnej jest to, że ponieważ program i specyfikacja to dwie oddzielne implementacje, ich błędy będą różne. Ale nie zawsze: jedno wspólne źródło błędów, przeoczone przypadki, często pasuje. Zatem weryfikacja formalna nie jest panaceum: nadal może przeoczyć nietrywialną liczbę błędów.

Wadą weryfikacji formalnej jest to, że może nałożyć około dwa razy więcej kosztów wdrożenia, prawdopodobnie więcej (potrzebujesz specjalista w zakresie specyfikacji formalnej i musisz użyć mniej lub bardziej eksperymentalnych narzędzi, które są z nią związane; to nie będzie tanie).

Myślę, że konfigurowanie przypadków testowych i rusztowań do ich uruchamiania automatycznie lepiej wykorzystasz Twój czas.

Komentarze

• Zaletą weryfikacji formalnej jest to, że … . Drugą wadą weryfikacji formalnej jest to, że … To jest mylące.
• Myślę, że niezgodność między specyfikacją a nieformalnym zadaniem jest kwestią analizy wymagań oprogramowania, a nie problemem programistycznym.

Zadajesz kilka różnych pytań. Zgadzam się, wydaje się, że formalne metody weryfikacji dla zastosowań przemysłowych / komercyjnych nie są tak powszechne. należy jednak zdawać sobie sprawę, że wiele zasad „weryfikacji formalnej” jest wbudowanych w kompilatory, aby określić poprawność programu! więc w pewnym sensie, jeśli używasz nowoczesnego kompilatora, „używasz większości najnowocześniejszych metod weryfikacji formalnej.

Mówisz„ Mam dość testowania ”, ale weryfikacja formalna tak naprawdę nie zastępuje testowania. w pewnym sensie jest to odmiana testowania.

Wspomniałeś o Javie.istnieje wiele zaawansowanych metod weryfikacji formalnej wbudowanych w program weryfikacyjny java o nazwie FindBugs , które rzeczywiście można uruchomić na dużych bazach kodu. Zauważ, że pokaże zarówno „fałszywie pozytywne, jak i fałszywie negatywne wyniki”, a wyniki muszą zostać sprawdzone / przeanalizowane przez ludzkiego programistę. Ale zauważ, że nawet jeśli nie ujawnia prawdziwych błędów funkcjonalnych, generalnie pojawia się „antywzory”, których i tak powinno się unikać w kodzie.

Nie wspominasz więcej o swojej aplikacji poza „przemysłową” . Formalna weryfikacja w praktyce zwykle zależy od konkretnego zastosowania.

Formalne techniki weryfikacji wydają się być szeroko stosowane w EE do udowodnienia poprawności obwodu, np. w projektowaniu mikroprocesorów.

Oto przykład przeglądu narzędzi weryfikacji formalnej w dziedzinie EE przeprowadzony przez Lars Philipson .

Komentarze

• Nie ' stwierdzenie, że ” a Wiele zasad ” formalnej weryfikacji ” jest wbudowanych w kompilatory w celu określenia poprawności programu „. To, o czym mówisz, to statyczne sprawdzanie typu, które robią niektóre kompilatory, ale właściwości zweryfikowane w ten sposób są raczej proste, np. unikanie dodawania liczby i ciągu. Jest to przydatne, ale dalekie od tego, co zwykle jest niedoceniane przez ” weryfikację formalną „.
• nie odnoszą się konkretnie do sprawdzania typu statycznego, chociaż jest to jeden prosty / powszechny przykład. Techniki optymalizacji kompilatora imho, które są szeroko rozpowszechnione i zaawansowane, są z grubsza podobne do zasad weryfikacji formalnej, ponieważ obejmują zaawansowane techniki określania / wykazywania równoważności zoptymalizowanych wariantów programu. dlatego wydaje się, że ważne jest, aby unikać problemu ” z ruchomymi słupkami bramki ” i nie zakładać, że tylko dlatego, że kompilator to robi lub jest zbudowany do kompilatora, jego nieformalna weryfikacja.
• zgodził się, że nie jest to powszechne rozumienie. Techniki optymalizacji z grubsza tworzą model zachowania programu, np. pętli lub podprogramu, i optymalizują ten model, a następnie generują nowy kod, który jest równoważny. dlatego niektóre z tych optymalizacji są dość zaawansowane w przestawianiu kodu &, według mnie wykorzystują one formalne zasady weryfikacji. wydaje się, że istnieje wiele innych przykładów formalnych metod weryfikacji w kompilatorze … pierwotne pytanie zadawało wiele różnych pytań, jak wielu zauważyło, zdecydowanie nie próbuję odpowiedzieć na wszystkie zawarte w nim pytania.
• sposób wydaje się, że istnieją pewne formalne zasady weryfikacji używane również w środowisku JRE, silniku wykonawczym java, np. optymalizacja dynamiczna itp.
• czyli ” marzenie o formalnej weryfikacji „, o której wspomniał filmus powyżej, imho jest chimeryczną abstrakcją, a pragmatyczny / utylitarny / realistyczny przemysł w dużej mierze to rozpoznaje. duże bazy kodów są znane od dziesięcioleci z natury, że mają x $ błędów / defektów na $ y $ K-linii kodu i to nigdy się nie zmieni bez względu na postęp teorii / technologii, to fakt ludzka natura. w rzeczywistości twierdzenia matematyczne stworzone przez człowieka mają te same właściwości, chociaż nie jest to powszechnie doceniane!

Może przydać się narzędzie do sprawdzania modeli.

http://alloytools.org/documentation.html Stop to narzędzie do sprawdzania modeli .

Ładna prezentacja wyjaśniająca koncepcję sprawdzania modelu za pomocą Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

W tej samej rodzinie narzędzi jest „testowanie oparte na właściwościach”, wszystkie próbują znaleźć kontrprzykład dla danego modelu specyfikacji twojego oprogramowania.