Formalna specyfikacja - Formal specification

W informatyce , specyfikacje formalne są techniki oparte matematycznie, których celem jest pomoc z wdrażaniem systemów i oprogramowania. Są one używane do opisywania systemu, analizowania jego zachowania i pomocy w jego projektowaniu poprzez weryfikację kluczowych właściwości zainteresowania za pomocą rygorystycznych i skutecznych narzędzi wnioskowania. Specyfikacje te są formalne w tym sensie, że mają składnię, ich semantyka mieści się w jednej dziedzinie i można z nich wywnioskować przydatne informacje.

Motywacja

Z każdą mijającą dekadą systemy komputerowe stawały się coraz potężniejsze i w rezultacie wywierały większy wpływ na społeczeństwo. Z tego powodu potrzebne są lepsze techniki pomagające w projektowaniu i wdrażaniu niezawodnego oprogramowania. Ugruntowane dyscypliny inżynierskie wykorzystują analizę matematyczną jako podstawę tworzenia i walidacji projektu produktu. Formalne specyfikacje są jednym ze sposobów osiągnięcia tego w niezawodności inżynierii oprogramowania, jak kiedyś przewidywano. Inne metody, takie jak testowanie, są częściej używane w celu poprawy jakości kodu.

Zastosowania

Mając taką specyfikację , możliwe jest zastosowanie technik weryfikacji formalnej w celu wykazania, że ​​projekt systemu jest poprawny w odniesieniu do jego specyfikacji. Pozwala to na weryfikację nieprawidłowych projektów systemu przed dokonaniem większych inwestycji w rzeczywiste wdrożenie. Innym podejściem jest użycie prawdopodobnie poprawnych kroków doprecyzowania w celu przekształcenia specyfikacji w projekt, który ostatecznie jest przekształcany w implementację poprawną pod względem konstrukcji .

Należy zauważyć, że formalna specyfikacja nie jest implementacją, ale raczej może być wykorzystana do opracowania implementacji . Formalne specyfikacje opisują, co system powinien robić, a nie jak powinien to robić.

Dobra specyfikacja musi posiadać kilka z następujących atrybutów: adekwatna, wewnętrznie spójna, jednoznaczna, kompletna, zadowolona, ​​minimalna

Dobra specyfikacja będzie miała:

  • Konstruowalność, zarządzalność i ewoluowalność
  • Użyteczność
  • Komunikatywność
  • Potężna i wydajna analiza

Jednym z głównych powodów zainteresowania formalnymi specyfikacjami jest to, że zapewniają one możliwość wykonywania dowodów na implementacje oprogramowania. Dowody te mogą być wykorzystane do walidacji specyfikacji, weryfikacji poprawności projektu lub do udowodnienia, że ​​program jest zgodny ze specyfikacją.

Ograniczenia

Sam projekt (lub wdrożenie) nigdy nie może zostać uznany za „poprawny”. Może być tylko „poprawna w stosunku do danej specyfikacji”. Odrębną kwestią jest to, czy formalna specyfikacja poprawnie opisuje problem do rozwiązania. Jest to również trudna kwestia do rozwiązania, ponieważ ostatecznie dotyczy problemu konstruowania wyabstrahowanych formalnych reprezentacji nieformalnej konkretnej dziedziny problemu , a taki krok abstrakcji nie podlega formalnemu dowodowi. Jednak możliwe jest zweryfikowanie specyfikacji poprzez udowodnienie „kwestionowanych” twierdzeń dotyczących właściwości, które ma wykazywać specyfikacja. Jeśli są poprawne, twierdzenia te wzmacniają rozumienie specyfikacji przez specyfikatora i jej związek z podstawową dziedziną problemu. Jeśli nie, prawdopodobnie należy zmienić specyfikację, aby lepiej odzwierciedlała rozumienie dziedziny przez osoby zaangażowane w tworzenie (i wdrażanie) specyfikacji.

Formalne metody wytwarzania oprogramowania nie są powszechnie stosowane w przemyśle. Większość firm uważa, że ​​stosowanie ich w procesach tworzenia oprogramowania nie jest opłacalne. Może to wynikać z różnych powodów, z których niektóre to:

  • Czas
    • Wysoki początkowy koszt rozruchu przy niskich mierzalnych zwrotach
  • Elastyczność
    • Wiele firm programistycznych stosuje metodyki zwinne, które koncentrują się na elastyczności. Wykonanie formalnej specyfikacji całego systemu z góry jest często postrzegane jako przeciwieństwo elastyczności. Istnieją jednak pewne badania nad korzyściami płynącymi z używania specyfikacji formalnych w przypadku programowania „zwinnego”
  • Złożoność
    • Wymagają wysokiego poziomu wiedzy matematycznej i umiejętności analitycznych, aby je zrozumieć i skutecznie zastosować
    • Rozwiązaniem tego byłoby opracowanie narzędzi i modeli, które pozwolą na wdrożenie tych technik, ale ukryją leżącą u ich podstaw matematykę
  • Ograniczony zakres
    • Nie wychwytują właściwości interesujących dla wszystkich interesariuszy projektu
    • Nie robią dobrej roboty przy określaniu interfejsów użytkownika i interakcji z użytkownikiem
  • Nieopłacalne
    • Nie jest to do końca prawdą, ponieważ ograniczają ich użycie tylko do podstawowych części krytycznych systemów, które okazały się opłacalne

Inne ograniczenia:

  • Izolacja
  • Ontologie niskiego poziomu
  • Słabe wskazówki
  • Słaba separacja obaw
  • Słaba opinia o narzędziach

Paradygmaty

Techniki specyfikacji formalnej istnieją od dłuższego czasu w różnych dziedzinach iw różnych skalach. Implementacje specyfikacji formalnych będą się różnić w zależności od rodzaju systemu, który próbują modelować, w jaki sposób są stosowane i w jakim momencie cyklu życia oprogramowania zostały wprowadzone. Tego typu modele można podzielić na następujące paradygmaty specyfikacji:

  • Specyfikacja oparta na historii
    • zachowanie na podstawie historii systemu
    • twierdzenia są interpretowane w czasie
  • Specyfikacja oparta na stanie
    • zachowanie oparte na stanach systemu
    • seria kolejnych kroków (np. transakcja finansowa)
    • języki takie jak Z , VDM czy B opierają się na tym paradygmacie
  • Specyfikacja oparta na przejściu
    • zachowanie oparte na przejściach ze stanu do stanu systemu
    • najlepiej stosować z systemem reaktywnym
    • języki takie jak Statecharts, PROMELA, STEP-SPL, RSML czy SCR opierają się na tym paradygmacie
  • Specyfikacja funkcjonalna
    • określić system jako strukturę funkcji matematycznych
    • OBJ, ASL, PLUSS, LARCH, HOL lub PVS polegają na tym paradygmacie
  • Specyfikacja operacyjna
    • wczesne języki, takie jak Paisley , GIST, sieci Petriego lub algebry procesów opierają się na tym paradygmacie

Oprócz powyższych paradygmatów istnieją sposoby zastosowania pewnych heurystyk, które pomogą ulepszyć tworzenie tych specyfikacji. Artykuł, do którego się tutaj odwołuje, najlepiej omawia heurystyki, które należy stosować podczas projektowania specyfikacji. Robią to, stosując podejście dziel i zwyciężaj .

Narzędzia programowe

Notacja Z jest przykładem wiodącego formalnej specyfikacji języka . Inne obejmują specyfikację Język (VDM-SL) o Metodzie Rozwoju Wiedeń i Abstract pralce Notation (AMN) z B-method . W obszarze usług sieci Web do opisu właściwości niefunkcjonalnych często stosuje się specyfikację formalną ( jakość usługi usług sieci Web ).

Niektóre narzędzia to:

Przykłady

Przykłady implementacji można znaleźć w linkach w sekcji narzędzia programowe .

Zobacz też

Bibliografia

Zewnętrzne linki