Jakie bariery uniemożliwiają powszechne przyjęcie metod formalnych? [Zamknięte]

Formalnych metod można użyć do określenia, udowodnienia i wygenerowania kodu dla aplikacji. Jest to mniej podatne na błędy - dlatego najczęściej stosowane w programach bezpieczeństwa / krytycznych.

Dlaczego nie używamy go częściej do codziennego programowania, aplikacji internetowych itp.?

Bibliografia :

• Metody formalne
• Metoda B.
• Hoare Logic

Inżynier to osoba, która może zrobić z dolarem to, co każdy idiota może zrobić z 10.

Ograniczenia zasobów, ograniczenia budżetowe, ograniczenia czasowe - wszystkie są ważne.

Tworzenie oprogramowania przy użyciu metod formalnych jest zwykle znacznie droższe i trwa znacznie dłużej niż bez niego. Ponadto w przypadku wielu projektów najtrudniejszą częścią jest zrozumienie wymagań biznesowych. Wszystko, co przy użyciu metod formalnych kupuje w takim przypadku, jest dowodem, że Twój kod odpowiada w 100% niekompletnemu i niepoprawnemu zrozumieniu wymagań biznesowych.

Z tego powodu stosowanie formalnych metod, dowodów, weryfikacji programu i podobnych technik jest zwykle ograniczone do „rzeczy, które mają znaczenie”, tj. Oprogramowania awioniki, systemów kontroli sprzętu medycznego, elektrowni itp.

Programować czy nie programować?

Aby rozwiązać problem z oprogramowaniem, po zapoznaniu się z wymaganiami możesz EITHER napisać program przy użyciu języków programowania LUB określić program przy użyciu języka formalnego i użyć narzędzi do generowania kodu. Ten ostatni dodaje poziom abstrakcji.

Czy robisz to dobrze, czy robisz dobrze?

Podejście formalne daje dowód, że oprogramowanie działa zgodnie ze specyfikacjami. Twój produkt robi to dobrze. Ale czy robi to dobrze?

Wymagania, nad którymi pracujesz, mogą być niepełne lub niejednoznaczne. Mogą nawet mieć problemy. W najgorszym przypadku rzeczywiste potrzeby nie są nawet wyrażone. Ale zdjęcie jest warte tysiąca słów, wystarczy użyć obrazów Google dla „Czego chce klient”, na przykład z tego artykułu :

Koszt formalności

W idealnym świecie od samego początku miałbyś w pełni szczegółowe i idealne wymagania. Następnie możesz w pełni określić swoje oprogramowanie. Jeśli zdecydujesz się na formalny, kod zostanie wygenerowany automatycznie, dzięki czemu będziesz bardziej produktywny. Wzrost wydajności zrównoważyłby koszty narzędzi formalnych. I wszyscy teraz używaliby metod formalnych. Dlaczego więc nie jest?

W praktyce rzadko jest to rzeczywistością! Właśnie dlatego tak wiele projektów wodospadu nie powiodło się i dlaczego wiodące były metody iteracyjne (zwinne, RAD itp.): Potrafią poradzić sobie z niekompletnymi i niedoskonałymi wymaganiami, projektami i implementacjami oraz dopracować je, dopóki nie będą w porządku.

I tu chodzi o sedno. W przypadku metod formalnych każda iteracja wymaga posiadania całkowicie spójnej specyfikacji formalnej. Wymaga to starannego myślenia i dodatkowej pracy, ponieważ logika formalna nie wybacza i nie lubi niekompletnych myśli. Proste eksperymenty z wyrzucaniem stają się kosztowne pod tym ograniczeniem. Podobnie dzieje się z każdą iteracją, która doprowadziłaby do wycofania się (np. Pomysł, który nie zadziałał lub wymaganie, które zostało źle zrozumiane).

W praktyce

Gdy nie jest się zobowiązanym do korzystania z metod formalnych z przyczyn prawnych lub umownych, można również osiągnąć bardzo wysoką jakość bez formalnych systemów, na przykład stosując programowanie oparte na umowie i inne dobre praktyki (np. Przegląd kodu, TDD itp.). Nie będziesz w stanie udowodnić, że twoje oprogramowanie działa, ale Twoi użytkownicy będą mogli cieszyć się działającym oprogramowaniem wcześniej.

Aktualizacja: zmierzony wysiłek

W wydanym w październiku 2018 r. Wydaniu Communications of ACM znajduje się interesujący artykuł na temat formalnie zweryfikowanego oprogramowania w świecie rzeczywistym, zawierający niektóre szacunki nakładu pracy.

Co ciekawe (w oparciu o rozwój systemu operacyjnego dla sprzętu wojskowego) wydaje się, że formalnie udowodnione oprogramowanie wymaga 3,3 razy więcej wysiłku niż w przypadku tradycyjnych technik inżynieryjnych. To jest naprawdę kosztowne.

Z drugiej strony, uzyskanie 2,3 razy mniejszego wysiłku, aby uzyskać oprogramowanie o wysokim bezpieczeństwie w ten sposób niż w przypadku tradycyjnie opracowanego oprogramowania, jeśli dodasz wysiłek, aby takie oprogramowanie było certyfikowane na wysokim poziomie bezpieczeństwa (EAL 7). Tak więc, jeśli masz wysokie wymagania dotyczące niezawodności lub bezpieczeństwa, to zdecydowanie jest uzasadnienie biznesowe do formalnego.

Projekt i opracowanie kodu seL4 zajęło dwie osoby na lata. Zsumowanie wszystkich dowodów serospecyficznych na przestrzeni lat daje w sumie 18 osobolat dla 8700 linii kodu C. Dla porównania, opracowanie L4Ka :: Pistachio, kolejnego mikrojądra w rodzinie L4, porównywalnego pod względem wielkości z seL4, zajęło sześć osobolat, i nie zapewnia znaczącego poziomu pewności. Oznacza to, że istnieje tylko współczynnik 3.3 między zweryfikowanym oprogramowaniem a tradycyjnie opracowanym oprogramowaniem. Według metody szacowania Colberta i Boehm'a 8, tradycyjna certyfikacja Common Criteria EAL7 dla 8700 linii kodu C zajęłaby ponad 45,9 osobolat. Oznacza to, że formalna weryfikacja implementacji na poziomie binarnym jest już ponad 2,3 mniej kosztowne niż najwyższy poziom certyfikacji Common Criteria, ale zapewnia znacznie lepszą pewność.

Każdy program w dowolnym języku może być traktowany jako formalna specyfikacja (odpowiednik jakiejś tokarki). Każda „formalna specyfikacja” wyższego poziomu, którą należy zastosować w celu udowodnienia poprawności formalnej, jest także - po prostu innym programem. Ale to (zwykle) zły, niekompletny, niejasny, niewystarczająco przemyślany program. I nieprzypadkowo, zwykle napisane przez ludzi, którzy nie wiedzą, jak programować (zwykle są ekspertami w dziedzinie).

Udowadniając, że jeden program jest kompatybilny (daje te same odpowiedzi lub niezależnie od tego, jak go charakteryzujesz) z jego wymogami formalnymi wyższego poziomu, niezmienny sprowadza się do sposobu rozwiązywania dwuznaczności w specyfikacji formalnej wyższego poziomu. Nie ma na to dobrego sposobu ogólnego przeznaczenia.

To odwzorowanie wymagań wysokiego poziomu na szczegóły niższego poziomu stanowi sedno prawdziwego programowania. Nie powinno dziwić, że podstawowa praca wykonywana przez programistę czytającego i interpretującego specyfikację nie może być zastąpiona machaniem ręką i mówieniem „teraz wystarczy sprawdzić, czy ten przykładowy program spełnia tę wysoką specyfikację formalną”.

Nawet we wczesnych dniach programowania logicznego, gdzie ta koncepcja wydawała się tak obiecująca (ponieważ zarówno specyfikacja wysokiego poziomu, jak i rzeczywiste programy bazowe mogły być napisane w tym samym języku), ten podstawowy problem okazał się trudny do rozwiązania.