Formalna weryfikacja programu w praktyce

66

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ą?

programming-languages  program-correctness  software-verification 
— Szczery
źródło
3
Rozumiem twój problem, ale nie rozumiem, po co jest to pytanie (jako post SE). Dyskusja? Doświadczenie? Żadne z nich nie jest odpowiednie dla SE. „Co mogę zrobić?” ton sprawia, że ​​czuję, że to zbyt szerokie pytanie.
— Raphael
3
Rozumiem ... Zgadzam się, że to pytanie nie zostało sformułowane jasno. Powiedzmy, że: 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 czy Coq wygeneruje z niego C ++ / Java? 4) Czy to podejście może poradzić sobie z optymalizacją wątków i wydajnością?
— Frank
2
Więc to są cztery pytania. 1) jest prawdopodobnie lepiej w inżynierii oprogramowania, ponieważ jest mało prawdopodobne, że spotkasz tutaj (wielu) specjalistów z branży. 2) smakuje nieco subiektywnie, ale możemy mieć tutaj ludzi, którzy mogą zaoferować obiektywną perspektywę. 3) jest, o ile wiem, całkowicie subiektywna. 4) Czy fajne pytania dotyczące tej strony. Podsumowując: proszę oddzielić swoje pytania, przejdź do Inżynierii oprogramowania w pierwszej kolejności i zastanów się, czy możesz spodziewać się obiektywnej (!) Odpowiedzi tutaj (!) Przed wysłaniem 2).
— Raphael
10
Opisujesz marzenie o formalnej weryfikacji, ale daleko nam do bycia tam. AFAIK, weryfikacja programu jest nietypowym zadaniem i dotyczy tylko bardzo prostych programów. To powiedziawszy, myślę, że to pytanie jest trafne dla strony i byłbym wdzięczny za to, że ktoś z tego obszaru przyznałby się do ograniczeń swojej dziedziny, wyjaśniając najnowocześniejsze i ograniczenia (być może poprzez link do jakiejś ankiety ).
— Yuval Filmus,
9
Problem z weryfikacją programów C ++ polega na tym, że C ++ nie jest dobrze zdefiniowanym językiem. Nie sądzę, aby weryfikacja na dużą skalę była możliwa, dopóki wiele części systemów oprogramowania (system operacyjny, biblioteki, języki programowania) nie zostanie przeprojektowanych w celu obsługi weryfikacji. Jak dobrze wiadomo, nie można po prostu zrzucić na kogoś 200 000 linii kodu i powiedzieć „zweryfikuj!”. Musisz zweryfikować i napisać kod razem, a także dostosować swoje nawyki programistyczne do faktu, że również weryfikujesz.
— Andrej Bauer,

Odpowiedzi:

35

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.

— cody
źródło
Dzięki za ten post i dodane referencje. IMHO, celem inżynierów oprogramowania jest możliwość szybkiego wypuszczenia systemów, które 1) zawsze zapewnią prawidłowe wyniki, 2) nigdy nie zawiodą. Widziałem tutaj problem z regresją, w którym możesz chcieć udowodnić, że sama specyfikacja jest „wolna od błędów” :-) to coś w rodzaju próby zdefiniowania „prawdziwej propozycji języka” za pomocą metajęzyka, a następnie potrzeby użycia innej meta język do tego, potem jeszcze jeden ...
— Frank
6
Problem polega na tym, że to, czego „chce” użytkownik, zwykle nie jest wyrażone w języku formalnym! Na ogół nie ma formalnej odpowiedzi na pytanie: „czy ta formalna specyfikacja jest zgodna z moim nieformalnym pomysłem?”. Można przetestować specyfikację formalną i udowodnić, że ma ona pewne właściwości matematyczne, ale ostatecznie trzeba powiązać matematykę ze światem rzeczywistym, co jest procesem nieformalnym.
— cody
Tak, oczywiście - zawsze zdawałem sobie sprawę, że metody formalne można zacząć tylko od ściśle określonego punktu. Jeśli ta specyfikacja jest zgodna ze świadomymi / nieświadomymi / nieodkrytymi potrzebami rzeczywistych użytkowników lub nie, jest to kolejny problem, którego nie można rozwiązać za pomocą metod formalnych (ale z pewnością problem inżynierów).
— Frank,
Twierdzenie jest z definicji sprawdzoną propozycją. Prawdopodobnie nie masz na myśli „udowodnić twierdzenia”.
— nro
@nbro Wikipedia wydaje się z tobą zgadzać. Mathworld definiuje jednak twierdzenie, które jest twierdzeniem, które „ można udowodnić, że jest prawdziwe przez zaakceptowane operacje matematyczne”. W takim przypadku przedstawienie dowodów twierdzeń jest nie tylko możliwe, ale konieczne, aby uzasadnić ich nazywanie! :) (oczywiście jest to sprzeczne)
— cody
15

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.

— hengxin
źródło
4

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.

— vonbrand
źródło
Zaletą weryfikacji formalnej jest to, że .... Drugą wadą weryfikacji formalnej jest to, że ... To jest mylące.
— hengxin
Myślę, że niedopasowanie specyfikacji do nieformalnego zadania jest kwestią analizy wymagań oprogramowania, a nie kwestią programowania.
— Kaveh
3

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.

— dc42
źródło
5
Dzięki za linki. Przydałby się przynajmniej krótki przegląd ich zawartości, aby uchronić się przed zepsuciem linków, zwłaszcza, że ​​twoje linki prowadzą do korporacyjnej strony internetowej: te mają tendencję do okresowej reorganizacji, zabijając wszystkie linki do strony.
— David Richerby,
2

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 .

— vzn
źródło
2
Mylące jest twierdzenie, że „wiele zasad„ formalnej weryfikacji ”jest wbudowanych w kompilatory w celu ustalenia poprawności programu”. To, o czym mówisz, to statyczne sprawdzanie typów, które robią niektóre kompilatory, ale właściwości zweryfikowane w ten sposób są raczej proste, np. Unikając dodawania liczby i łańcucha. Jest to pomocne, ale dalekie od tego, co zwykle rozumie się przez „formalną weryfikację”.
— Martin Berger,
2
nie odnosi 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 formalnych zasad weryfikacji, ponieważ obejmują zaawansowane techniki określania / pokazywania równoważności zoptymalizowanych wariantów programu. Wydaje się więc, że ważne jest, aby unikać problemu „ruchomych słupków bramki” i nie zakładać, że tylko dlatego, że kompilator to robi lub jest wbudowany w kompilator, nie jest to formalna weryfikacja.
— vzn
2
zgodzili się, że nie jest to powszechne porozumienie. 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 można udowodnić. więc niektóre z tych optymalizacji są dość wyrafinowane w przestawianiu kodu i dla mnie wykorzystują 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 zauważyło wielu, nie staram się odpowiadać na wszystkie zawarte w nim pytania.
— vzn 23.08.13
2
nawiasem mówiąc, wydaje się, że istnieją pewne formalne zasady weryfikacji stosowane również w JRE, java runtime engine, np. optymalizacja dynamiczna itp.
— vzn 24.08.2013
3
to jest „ marzenie o formalnej weryfikacji”, o którym mowa w powyższym filmie, imho jest chimeryczną abstrakcją, a pragmatyczny / utylitarny / realistyczny przemysł w dużej mierze uznaje to za takie. duże codebases były znane od dziesięcioleci do natury mają błędy / usterki za K-linii kodu i będzie to nigdy nie zmieni bez względu na to jaki postęp teoria / Technology, jej fakt ludzkiej natury. i w rzeczywistości stworzone przez człowieka twierdzenia matematyczne mają te same właściwości, chociaż nie jest to powszechnie doceniane! yxy
— vzn
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.