Jak stworzyć oprogramowanie krytyczne dla misji?

Uczę się metod formalnych. Słyszałem, że do tworzenia oprogramowania o kluczowym znaczeniu (takiego jak kontroler reaktora jądrowego, kontroler lotu statku powietrznego, kontroler sondy kosmicznej) stosuje się (i zwykle stosuje się) metody formalne. Dlatego chcę się tego nauczyć: str

Jednak po zapoznaniu się z metodami formalnymi (zwłaszcza LTL, CTL i ich rodzeństwem) czuję, że można ich użyć tylko do weryfikacji poprawności specyfikacji (bezpieczeństwo, żywotność, uczciwość itp.).

Ale jak sprawdzić, czy oprogramowanie (nie tylko specyfikacja) jest rzeczywiście poprawne?

Zastrzeżenie: Jestem 90% idiotą, jeśli chodzi o informatykę teoretyczną. Prosimy więc o litość podczas odpowiadania.

Pytanie jest dość ogólne. Aby odpowiedzieć na to pytanie w rozsądnej przestrzeni, dokonam wielu uproszczeń.

Uzgodnijmy terminologię. Program jest poprawny, jeśli sugeruje jego specyfikację. To niejasne stwierdzenie jest precyzyjne na wiele sposobów, poprzez określenie, czym dokładnie jest program, a co dokładnie specyfikacją. Na przykład podczas sprawdzania modelu program ma strukturę Kripke, a specyfikacja jest często formułą LTL . Lub, program może być listą instrukcji PowerPC, a specyfikacją może być zestaw twierdzeń Hoare-Floyda zapisanych, powiedzmy, w logice pierwszego rzędu. Istnieje bardzo wiele możliwych wariantów. Kuszące jest stwierdzenie, że w jednym przypadku (struktura Kripke) nie weryfikujemy rzeczywistego programu, podczas gdy w drugim przypadku (lista instrukcji PowerPC) to robimy. Jednak ważne jest, aby zdać sobie sprawę, że naprawdę przyglądamy się modelom matematycznym w obu przypadkach, i jest to całkowicie w porządku. (Sytuacja jest bardzo podobna do fizyki, gdzie na przykład mechanika klasyczna jest matematycznym modelem rzeczywistości).

Większość formalizacji rozróżnia składnię i semantykę programu; to znaczy, w jaki sposób jest reprezentowany i co to znaczy. Z punktu widzenia weryfikacji programu liczy się semantyka programu. Ale oczywiście ważne jest, aby mieć jasny sposób przypisywania znaczeń programom (składnie) programów. Dwa popularne sposoby to:

• (mały krok) semantyka operacyjna : Jest to bardzo podobne do definiowania języka programowania przez napisanie dla niego tłumacza. W tym celu musisz powiedzieć, jaki jest stan , na który wpływa każde zdanie w języku. (Możesz się zastanawiać, w jakim języku piszesz tłumacza, ale udam, że nie.)
• semantyka aksjomatyczna : tutaj każdy typ instrukcji ma schemat aksjomatyczny. Z grubsza, za każdym razem, gdy używane jest określone stwierdzenie tego typu, przekłada się to na możliwość używania pewnych aksjomatów. Na przykład przypisanie ma schemat { P [ x / e ] ${\bf x}:={\bf e}$ ; dane przypisanie x : = x + 1 ma aksjomat { x + 1 = 1 $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$$x:=x+1$ jeśli utworzymy instancję schematu za pomocą P = ( x = 1 ) .$\{x+1=1\}\,x:=x+1\,\{x=1\}$$P=(x=1)$

(Są inne. Szczególnie źle czuję się, gdy pomijam semantykę denotacyjną, ale ta odpowiedź jest już długa.) Kod maszynowy i semantyka operacyjna są bardzo zbliżone do tego, co większość ludzi nazwałaby „prawdziwym programem”. Oto kluczowy artykuł, który wykorzystuje semantykę operacyjną dla podzbioru kodu maszynowego DEC Alpha:

• Necula, Lee, Proof-Carrying Code , 1996

Dlaczego miałbyś kiedykolwiek używać semantyki wyższego poziomu, takiej jak aksjomatyczna? Gdy nie chcesz, aby Twój dowód poprawności był zależny od sprzętu, na którym działasz. Podejście polega zatem na udowodnieniu poprawności algorytmu w odniesieniu do pewnej wygodnej semantyki wysokiego poziomu, a następnie udowodnieniu, że semantyka brzmi w odniesieniu do semantyki niższego poziomu, które są bliższe rzeczywistym maszynom.

Podsumowując, mogę wymyślić trzy przyczyny, które doprowadziły do ​​twojego pytania:

1. Widziałeś tylko semantykę wysokiego poziomu, która nie wygląda tak, jak zwykłaś nazywać program, i zastanawiasz się, czy są semantyki niskiego poziomu. Odpowiedź brzmi tak.
2. Zastanawiasz się, jak udowodnić, że model odpowiada rzeczywistości. Podobnie jak w fizyce, nie. Po prostu wymyślasz lepsze modele i porównujesz je z rzeczywistością.
3. Nie widziałeś rozróżnienia między składnią i semantyką oraz różnymi sposobami przypisywania znaczenia programom. Dwa poprzednie pytania wymieniają niektóre książki.

Ta odpowiedź próbuje jedynie zidentyfikować trzy różne sposoby, w jakie zrozumiałem pytanie. Wchodzenie głęboko w którykolwiek z tych punktów wymagałoby dużo miejsca.

Jednym ze sposobów zmniejszenia luki między programem a jego specyfikacją jest użycie języka z formalną semantyką. Ciekawym przykładem byłaby tutaj Esterel . Zajrzyj na stronę internetową Gérarda Berry'ego, gdzie znajdziesz ciekawe rozmowy na temat jego pracy nad wprowadzeniem metod formalnych do realnego świata. http://www-sop.inria.fr/members/Gerard.Berry/

ps Byłeś na Airbusie? Leciałeś metodami formalnymi!

Nauka budowy niezawodnego oprogramowania w „prawdziwym świecie” jest wciąż rozwijana i do pewnego stopnia opiera się na badaniach z natury kulturowych lub antropologicznych, ponieważ komputery i oprogramowanie nie „powodują” błędów - ludzie tak robią! odpowiedź ta skupi się na ogólnych podejściach do pytań / odpowiedzi, których formalną weryfikację oprogramowania można postrzegać jako jeden element.

niezwykłą spostrzeżeniem jest to, że często oprogramowanie, które jest „wystarczająco dobre”, ale „błędne”, często może wyprzedać lepiej przetestowane, ale o niższej funkcjonalności oprogramowanie na rynku. innymi słowy, rynek nie zawsze kładzie nacisk na jakość oprogramowania i nowoczesne techniki inżynierii oprogramowania, które nie zawsze kładą nacisk na jakość, nieco to odzwierciedlają. ponadto jakość może często stanowić znaczny wydatek na produkt końcowy. z tymi zastrzeżeniami, oto niektóre z podstaw:

• systemy redundantne / odporne na uszkodzenia. jest to szeroki obszar badań. tolerancję i redundancję błędów można zaprojektować w wielu warstwach systemu. np. router, serwer, napęd dyskowy itp.

• testowanie . wszystkie typy - testy jednostkowe, testy integracyjne, testy akceptacyjne użytkownika, testy regresyjne itp.

• obecnie zautomatyzowane testowanie za pomocą pakietów testowych, które można uruchamiać bez nadzoru, jest bardziej rozbudowane / ważne. działające zestawy testowe są często połączone z narzędziem do budowania.

• ważną koncepcją w testowaniu jest pokrycie kodu . tj. jaki kod jest wykonywany przez test. test nie może znaleźć błędu w kodzie, który nie jest „dotknięty” przez test.

• Inną kluczową koncepcją w testach jest testowanie tego kodu ćwiczeń, do którego dostęp nie jest łatwy.

• testy powinny wykonywać wszystkie poziomy oprogramowania. jeśli oprogramowanie jest dobrze zmodularyzowane, nie jest to trudne. testy wyższego poziomu powinny wnikać głęboko w kod. testy wykorzystujące duże ilości kodu przy małej konfiguracji testu zwiększają „dźwignię testową” .

• Sprawienie, by kod był jak najmniej skomplikowany, jest możliwe do testowania. testy powinny być brane pod uwagę przy projektowaniu architektury. często istnieje wiele sposobów implementacji tej samej funkcji, ale niektóre mają wiele różnych implikacji dla zasięgu testowania / dźwigni. dla każdej gałęzi kodu jest to często kolejny przypadek testowy. gałęzie w gałęziach rosną do wykładniczego wzrostu ścieżek kodu. dlatego unikanie mocno zagnieżdżonej / warunkowej logiki poprawia zdolność do testowania.

• badanie słynnych (ogromnych) awarii oprogramowania, których jest wiele przykładów, a studia przypadków są pomocne w zrozumieniu historii i rozwijaniu sposobu myślenia ukierunkowanego na względy jakościowe.

• można dać się ponieść testom! istnieje zarówno problem ze zbyt małym, jak i zbyt dużym testowaniem. jest „słodkie miejsce”. oprogramowania nie można z powodzeniem wbudować ani w ekstremalne.

• korzystaj ze wszystkich podstawowych narzędzi w najbardziej efektywny sposób. debuggery, profilery kodu, narzędzia pokrycia kodu testowego, system śledzenia defektów itp! niekoniecznie zobowiązują się do naprawy, ale śledzą nawet najmniejsze wady oprogramowania śledzącego.

• staranne stosowanie SCM, zarządzanie kodem źródłowym i techniki rozgałęziania jest ważne w celu uniknięcia regresji, izolowania i postępu poprawek itp.

• Programowanie w wersji N : praktyka często używana do tworzenia oprogramowania o znaczeniu krytycznym. Założeniem tej praktyki jest to, że N niezależnie opracowanych programów raczej nie ma tego samego wspólnego błędu / usterki. Zostało to skrytykowane w kilku artykułach . NVP jest jednak praktyką, a nie koncepcją teoretyczną.

Wierzę, że fizyk Feynman ma w swojej książce „Metodę NASA w celu zagwarantowania niezawodności systemów wahadłowców”. Co cię obchodzi, co myślą inni? - powiedział, że mają dwie drużyny, powiedzmy, że zespół A i zespół B. zbudowali oprogramowanie. drużyna B przyjęła przeciwne podejście do Drużyny A i próbowała złamać oprogramowanie.

pomaga to, jeśli Zespół B ma dobre przygotowanie inżynieryjne, tzn. że sami mogą pisać wiązkę kodu / testy programowe itp. w takim przypadku Zespół B miał prawie taki sam poziom zasobów jak Zespół A. Z drugiej strony takie podejście jest drogie, ponieważ może prawie podwoić koszty budowy oprogramowania. częściej jest to mniejszy zespół ds. kontroli jakości w porównaniu do zespołu programistów.

Stare podejście (ale nadal jest używane w niektórych aplikacjach) to programowanie w wersji N.

Z Wikipedii:

Programowanie w wersji N ( NVP ), znane również jako programowanie w wielu wersjach , jest metodą lub procesem inżynierii oprogramowania, w którym wiele funkcjonalnie równoważnych programów jest generowanych niezależnie na podstawie tych samych specyfikacji początkowych. Koncepcja programowania w wersji N została wprowadzona w 1977 r. Przez Liming Chen i Algirdasa Avizienisa z centralnym przypuszczeniem, że „niezależność wysiłków programistycznych znacznie zmniejszy prawdopodobieństwo wystąpienia identycznych błędów oprogramowania w dwóch lub więcej wersjach programu”. Cel NVP ma na celu poprawę niezawodności działania oprogramowania poprzez budowanie tolerancji na błędy lub redundancji.
…

Zobacz na przykład: „ Wyzwania w usterce budynku - tolerancyjny system sterowania lotem dla samolotu cywilnego ”

fajrian, to pytanie, które postawiłeś, obejmuje dwa największe problemy w badaniach inżyniera oprogramowania: zgodność specyfikacji ze modelem oraz między modelem a kodem. Modeluj tutaj reprezentację tego, co zrobi system lub jak to będzie zrobione, istnieje wiele poziomów do modelowania systemu.

Są ludzie, którzy próbują znaleźć najlepszą odpowiedź na twoje pytanie. Ponieważ bardzo trudno jest sprawdzić poprawność oprogramowania opartego na modelu, na przykład przy użyciu metod formalnych. Znam JML jest na to sposobem, ale nie znam granic jego używania.

Podsumowując, jak trudno jest sprawdzić poprawność kodu, ludzie próbują łączyć metody formalne i testować, tworząc testy automatycznie na przykład ze specyfikacji. Jednym z przykładów systemów czasu rzeczywistego jest TIOSTS oparty na zdarzeniach czasowych wejścia / wyjścia.

Tylko testowanie nie jest formalnym podejściem metodycznym, ponieważ poprawia niezawodność, ale nie sprawdza poprawności.

Dwa lub trzy lata temu zacząłem przyglądać się formalnym metodom stosowanym w oprogramowaniu. Było to zadanie napędzane ciekawością i poczuciem, że musiałem nauczyć się narzędzi i metod programowania z dłuższymi okresami. Chociaż marzyłem życzliwie o Srebrnej Kuli , naprawdę myślałem, że nie ma odpowiedzi na pytanie: „Jak napisać poprawny program?”.

W tym momencie wyprawy po wypróbowaniu niektórych narzędzi (Z, B, VHDL i Estelle) używam TLA + . Jest to wariant logiki czasowej z narzędziami programowymi do sprawdzania modelu i prób mechanicznych. Myślę, że wybrałem to podejście, ponieważ L. Lamport był za tym, składnia była prosta, było wiele przykładów, istniała społeczność, a język i narzędzia były dość dobrze udokumentowane.

Jeśli chodzi o moje pierwsze pytanie, myślę, że nie ma pełnej odpowiedzi. Warto jednak nauczyć się, że opłaca się formalnie określać niektóre części systemu. Przydaje się również inżynieria wsteczna niektórych złożonych. Oznacza to, że skuteczne jest stworzenie planu dla trudnych i krytycznych części. Nie sądzę jednak, aby istniała skuteczna metoda automatycznego tłumaczenia specyfikacji na język programowania lub środowisko programistyczne (chyba że ograniczysz projekt do bardzo specyficznego środowiska). Nie uważam też, że posiadanie formalnej specyfikacji powinno uniemożliwić testowanie oprogramowania.

W skrócie, myślę, że następująca metafora (z Lamport) jest naprawdę potężna: „Czy spodziewasz się, że dom zostanie automatycznie zbudowany na podstawie planu? Czy kupisz dom, który nie został jeszcze zbudowany i nie ma planu?” .

Podczas tego zadania znalazłem przydatne zasoby:

• Metody specyfikacji oprogramowania . Ta książka zawiera szeroki przegląd istniejących metod i narzędzi. Można tam znaleźć podstawowe wyjaśnienia i przykłady Z, SDL, TLA +, sieci Petriego, Coq itp.
• Jeśli uważasz, że TLA + odpowiada Twoim potrzebom, naprawdę polecam książkę Specifying Systems . Możesz dostać książkę za darmo, a ona zawiera przykłady do zabawy :).
• Niedawno przeczytałem kilka powiązanych artykułów, które przedstawiają dwie różne perspektywy najnowocześniejszych metod formalnych: przypadek metod formalnych i matematyka formalnie zweryfikowana .

Powodzenia!

Dotychczasowe odpowiedzi obejmowały już większość tego, co należy powiedzieć o podstawach wzajemnego powiązania specyfikacji i kodu. Chcę tylko dodać bardziej praktyczny punkt, który zbliża się do pytania w nagłówku tego wątku:

Jak stworzyć oprogramowanie o znaczeniu krytycznym?

Istnieją narzędzia, które automatycznie analizują kod pod kątem błędów (naruszenia specyfikacji lub „typowe błędy”). Według mojej wiedzy metody te opierają się głównie na analizie statycznej i nie są bezpośrednio związane z teoriami, o których wspominałeś (LTL / CTL / ...), ale znajdują błędy w prawdziwym kodzie i jest to już wykonalne, z praktycznego punktu widzenia zobacz, aby korzystać z takich narzędzi w projektach przemysłowych. Osobiście nie korzystałem z wielu z nich, ale wydaje się, że narzędzia te zaczynają być akceptowane przez praktyków. Do dalszego czytania mogę polecić następujący artykuł na blogu:

http://www.altdevblogaday.com/2011/12/24/static-code-analysis/

Algorytmy certyfikujące mogą być przydatne podczas tworzenia oprogramowania o znaczeniu krytycznym.

Algorytm certyfikujący to algorytm, który przy każdym wyjściu wytwarza certyfikat lub świadek (łatwy do zweryfikowania dowód), że błąd nie wpłynął na dane wyjście.

Przeczytaj więcej w tym artykule ankietowym Algorytmy certyfikujące McConnell, RM i Mehlhorn, K. i Naher, S. i Schweitzer, P.

Ale jak sprawdzić, czy oprogramowanie (nie tylko specyfikacja) jest rzeczywiście poprawne?

Testów jednostkowych? Napisz test dla każdego wymagania w specyfikacji, a następnie przetestuj każdą metodę w swojej implementacji, aby sprawdzić, czy dane wyjściowe / wejściowe są zgodne z tą specyfikacją. Można to zautomatyzować, aby testy były przeprowadzane w sposób ciągły, aby żadna zmiana nigdy nie uszkodziła wcześniej działających funkcji.

Teoretycznie, jeśli testy jednostkowe obejmują 100% pokrycia kodu (tj. Testowana jest każda metoda w kodzie), oprogramowanie powinno być poprawne, pod warunkiem, że same testy są dokładne i realistyczne.