Formalna weryfikacja programu w praktyce

Jako inżynier oprogramowania piszę dużo kodu dla produktów przemysłowych. Stosunkowo skomplikowane rzeczy z klasami, wątkami, trochę wysiłków projektowych, ale także pewne kompromisy w zakresie wydajności. Robię dużo testów i mam dość testowania, więc zainteresowałem się narzędziami do sprawdzania formalnego, takimi jak Coq, Isabelle ... Czy mogę użyć jednego z nich, aby formalnie udowodnić, że mój kod jest wolny od błędów i gotowe z tym? - ale za każdym razem, gdy sprawdzam jedno z tych narzędzi, odchodzę nieprzekonany, że nadają się one do codziennej inżynierii oprogramowania. To może być tylko ja i szukam wskazówek / opinii / pomysłów na ten temat :-)

W szczególności odnoszę wrażenie, że sprawienie, by jedno z tych narzędzi działało, wymagałoby ogromnej inwestycji, aby właściwie zdefiniować obiekt, metody… rozważanego programu. Zastanawiam się wtedy, czy nie zabraknie mu pary, biorąc pod uwagę rozmiar wszystkiego, z czym będzie musiał sobie poradzić. A może musiałbym pozbyć się efektów ubocznych (te narzędzia do sprawdzania poprawności wydają się naprawdę dobrze radzić sobie z deklaratywnymi językami) i zastanawiam się, czy to spowodowałoby „sprawdzony kod”, którego nie można byłoby użyć, ponieważ nie byłby szybki lub wystarczająco mały. Poza tym nie mam luksusu zmieniać języka, z którym pracuję, musi to być Java lub C ++: Nie mogę powiedzieć mojemu szefowi, że od teraz będę pisać w OXXXml, ponieważ jest to jedyny język w co mogę udowodnić poprawność kodu ...

Czy ktoś z większym doświadczeniem w zakresie formalnych narzędzi sprawdzających może komentować? Znowu - ja kocham używać formalnego narzędzia Prover, myślę, że są świetne, ale mam wrażenie, że są w wieży z kości słoniowej, że nie może dotrzeć z ubogiej rowu Java / C ++ ... (PS: także UWIELBIAM Haskell, OCaml ... nie mam pomysłu: jestem fanem deklaratywnych języków i formalnego dowodu, próbuję tylko zobaczyć, jak mogę realistycznie uczynić to użytecznym dla inżynierii oprogramowania)

Aktualizacja: Ponieważ jest to dość szerokie, spróbujmy odpowiedzieć na następujące bardziej szczegółowe pytania: 1) czy istnieją przykłady użycia dowódców w celu udowodnienia poprawności przemysłowych programów Java / C ++? 2) Czy Coq byłby odpowiedni do tego zadania? 3) Jeśli Coq jest odpowiedni, czy powinienem najpierw napisać program w Coq, a następnie wygenerować C ++ / Java z Coq? 4) Czy to podejście może poradzić sobie z optymalizacją wątków i wydajnością?

Spróbuję udzielić zwięzłej odpowiedzi na niektóre pytania. Należy pamiętać, ż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 w celu formalnego udowodnienia właściwości Java i C ++.

   Muszę jednak tutaj zrobić małą dygresję: co to znaczy udowodnić poprawność programu? Kontroler typu Java potwierdza formalną właściwość programu Java, a mianowicie, że pewne błędy, takie jak dodanie a floati an int, nigdy nie mogą wystąpić! Wyobrażam sobie, że interesują cię znacznie silniejsze właściwości, a mianowicie to, że twój program nigdy nie może wejść w niechciany stan lub że dane wyjściowe określonej funkcji są zgodne z pewną specyfikacją matematyczną. Krótko mówiąc, istnieje szeroki gradient 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 zakładam, że jesteś zainteresowany udowodnieniem silnych właściwości swoich programów. Jeśli interesują Cię właściwości bezpieczeństwa (twój program nie może osiągnąć określonego stanu), to ogólnie rzecz biorąc wydaje się, że najlepszym rozwiązaniem jest sprawdzenie modelu . Jeśli jednak chcesz w pełni określić zachowanie programu Java, najlepszym rozwiązaniem jest użycie języka specyfikacji dla tego języka, na przykład JML . Istnieją takie języki do określania zachowania programów C, na przykład ACSL , ale nie wiem o C ++.

2. Po uzyskaniu specyfikacji musisz udowodnić, że program jest zgodny z tą specyfikacją.

   W tym celu potrzebujesz narzędzia, które ma formalne zrozumienie zarówno twojej specyfikacji, jak i semantyki operacyjnej twojego języka (Java lub C ++), aby wyrazić twierdzenie adekwatności , a mianowicie, że wykonanie programu jest zgodne ze specyfikacją.

   To narzędzie powinno także umożliwiać formułowanie lub generowanie dowodu tego twierdzenia. Teraz oba te zadania (określanie i sprawdzanie) są dość trudne, dlatego często dzieli się je na dwie części:

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

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

   Jedna (drobna) kwestia: istnieją pewne twierdzenia, które są zbyt trudne do udowodnienia za pomocą metod automatycznych, a wiadomo, że automatyczne dowody twierdzeń czasami zawierają błędy poprawności, które czynią je mniej wiarygodnymi. Jest to obszar, w którym Coq świeci w porównaniu (ale nie jest to automatyczne!).

3. Jeśli chcesz wygenerować kod Ocaml, zdecydowanie najpierw napisz w Coq (Gallina), a następnie wypakuj kod. Jednak Coq jest okropny w generowaniu C ++ lub Java, jeśli jest to w ogóle możliwe.

4. Czy powyższe narzędzia radzą sobie z problemami z gwintowaniem 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 tutaj jakieś narzędzia, które mogę polecić, choć projekt PolyNI Martina Hofmanna wydaje się interesujący.

Podsumowując: formalna weryfikacja programów Java i C ++ w „świecie rzeczywistym” jest dużą i dobrze rozwiniętą dziedziną, a Coq nadaje się do części tego zadania. Można znaleźć przegląd wysokiego poziomu tu na przykład.

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

1. Narzędzie Open Source Java Pathfinder (w skrócie JPF) wydane przez NASA w 2005 roku to system do weryfikacji wykonywalnych programów kodu bajtowego Java (patrz Java Pathfinder @ wiki ). Został on wykorzystany do wykrywania niespójności w oprogramowaniu wykonawczym dla K9 Rover w NASA Ames.

2. Ten artykuł: Korzystanie z funkcji sprawdzania modelu w celu znalezienia poważnych błędów w systemie plików @ OSDI'04 pokazuje, jak używać funkcji sprawdzania modelu w celu znalezienia poważnych błędów w systemach plików. System o nazwie FiSC jest stosowany do trzech powszechnie używanych, mocno przetestowanych systemów plików: ext3, JFS i ReiserFS, i znaleziono 32 poważne błędy. Zdobył nagrodę Best Paper Award.

3. Ten artykuł: Jak Amazon Web Services używa metod formalnych @ CACM'15 opisuje, w jaki sposób AWS stosuje metody formalne do swoich produktów, takich jak S3, DynamoDB, EBS i wewnętrzny menedżer zamków rozproszonych. Koncentruje się na narzędziu Lamport TLA + . Nawiasem mówiąc, Lamport intensywnie korzystał z własnego zestawu narzędzi TLA. Często dokonuje (całkowicie kompletnej) weryfikacji formalnej 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ć własne błędy.

Zaletą formalnej weryfikacji jest to, że ponieważ program i specyfikacja są dwiema odrębnymi implementacjami, ich błędy będą różne. Ale nie zawsze: jedno wspólne źródło błędów, pomijane przypadki, często do siebie pasuje. W związku z tym formalna weryfikacja nie jest panaceum: nadal może przeoczyć nietrywialną liczbę błędów.

Wadą weryfikacji formalnej jest to, że może ona nałożyć coś w rodzaju dwukrotności kosztów wdrożenia, prawdopodobnie więcej (potrzebujesz specjalisty w zakresie specyfikacji formalnej i musisz użyć mniej więcej eksperymentalnych narzędzi, które są z nią związane; to nie będzie tanie ).

Wydaje mi się, że skonfigurowanie przypadków testowych i rusztowań w celu ich automatycznego uruchomienia byłoby lepszym wykorzystaniem twojego czasu.

Formalna weryfikacja jest teraz możliwa dla programów napisanych w podzbiorze C ++ zaprojektowanych dla systemów wbudowanych o krytycznym znaczeniu dla bezpieczeństwa. Zobacz http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt do krótkiej prezentacji i http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf pełny papieru.

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

Mówisz „jestem zmęczony testowaniem”, ale formalna weryfikacja tak naprawdę nie zastępuje testowania. w pewnym sensie jest to wariacja na temat testowania.

Wspominasz o Javie. istnieje wiele zaawansowanych metod weryfikacji formalnej wbudowanych w program weryfikacji java o nazwie FindBugs, który w rzeczywistości można uruchomić na dużych bazach kodów. Zauważ, że pojawi się zarówno „fałszywie dodatni, jak i fałszywy negatyw”, a wyniki muszą zostać przejrzane / przeanalizowane przez człowieka. Należy jednak pamiętać, że nawet jeśli nie ujawnia on rzeczywistych defektów funkcjonalnych, generalnie pojawia się „antypattern”, którego i tak należy unikać w kodzie.

Nie wspominasz więcej o swoim konkretnym zastosowaniu poza „przemysłowym”. Formalna weryfikacja w praktyce zwykle zależy od konkretnego wniosku.

Wydaje się, że formalne techniki weryfikacji są szeroko stosowane w EE w celu udowodnienia poprawności obwodu, np. W projektowaniu mikroprocesora.

Oto przykład badania formalnych narzędzi weryfikacyjnych w dziedzinie EE przeprowadzonego przez Larsa Philipsona .

Być może pomocny może być moduł sprawdzania modelu.

http://alloytools.org/documentation.html Alloy to moduł sprawdzający model.

Ładna prezentacja wyjaśniająca koncepcję sprawdzania modelu przy użyciu stopu: https://www.youtube.com/watch?v=FvNRlE4E9QQ

W tej samej rodzinie narzędzi znajduje się „testowanie właściwości”, wszystkie one próbują znaleźć kontrprzykład dla danego modelu specyfikacji oprogramowania.