Formální specifikace - Formal specification

V informatice jsou formální specifikace matematicky založené techniky, jejichž účelem je pomoci s implementací systémů a softwaru. Používají se k popisu systému, k analýze jeho chování ak pomoci při jeho návrhu ověřováním klíčových vlastností, které nás zajímají, prostřednictvím přísných a efektivních nástrojů uvažování. Tyto specifikace jsou formální v tom smyslu, že mají syntaxi, jejich sémantika spadá do jedné domény a lze je použít k odvození užitečných informací.

Motivace

V každém dalším desetiletí se počítačové systémy staly stále výkonnějšími a v důsledku toho začaly mít pro společnost větší vliv. Z tohoto důvodu jsou při navrhování a implementaci spolehlivého softwaru zapotřebí lepší techniky. Zavedené inženýrské disciplíny používají matematickou analýzu jako základ pro vytváření a ověřování designu produktu. Formální specifikace jsou jedním ze způsobů, jak toho dosáhnout ve spolehlivosti softwarového inženýrství, jak se kdysi předpokládalo. Další metody, jako je testování, se běžně používají ke zlepšení kvality kódu.

Využití

Vzhledem k takové specifikaci je možné použít formální ověřovací techniky k prokázání, že návrh systému je správný s ohledem na jeho specifikaci. To umožňuje revizi nesprávných návrhů systému před provedením jakýchkoli větších investic do skutečné implementace. Dalším přístupem je použít pravděpodobně správné kroky upřesnění k transformaci specifikace na design, který je nakonec transformován do implementace, která je správná konstrukcí .

Je důležité si uvědomit, že formální specifikace není implementace, ale může být použita k vývoji implementace . Formální specifikace popisují, co by měl systém dělat, nikoli jak by to měl systém dělat.

Dobrá specifikace musí mít některé z následujících atributů: adekvátní, vnitřně konzistentní, jednoznačné, úplné, spokojené, minimální

Dobrá specifikace bude mít:

  • Konstrukovatelnost, ovladatelnost a vyvíjitelnost
  • Použitelnost
  • Komunikace
  • Výkonná a efektivní analýza

Jedním z hlavních důvodů, proč je zájem o formální specifikace, je to, že budou poskytovat schopnost provádět kontroly softwarových implementací. Tyto důkazy lze použít k ověření specifikace, ověření správnosti návrhu nebo k prokázání, že program splňuje specifikaci.

Omezení

Návrh (nebo implementaci) nelze nikdy sám prohlásit za „správný“. Vždy může být pouze „správné s ohledem na danou specifikaci“. Zda formální specifikace správně popisuje problém, který je třeba vyřešit, je samostatná otázka. Je to také obtížně řešitelný problém, protože se v konečném důsledku týká problému vytvářejícího abstrahované formální reprezentace neformální konkrétní problémové domény a takový krok abstrakce není přístupný formálnímu důkazu. Je však možné ověřit specifikaci prokázáním „provokačních“ vět týkajících se vlastností, které by měla specifikace vykazovat. Pokud jsou správné, tyto věty posilují porozumění specifikátoru specifikátoru a jeho vztah k základní problémové doméně. Pokud ne, je pravděpodobně nutné specifikaci změnit, aby lépe odrážela doménové chápání těch, kteří se podílejí na výrobě (a implementaci) specifikace.

Formální metody vývoje softwaru nejsou v průmyslu příliš využívány. Většina společností nepovažuje za nákladově efektivní použít je v procesech vývoje softwaru. To může být z různých důvodů, z nichž některé jsou:

  • Čas
    • Vysoká počáteční počáteční cena s nízkou měřitelnou návratností
  • Flexibilita
    • Mnoho softwarových společností používá agilní metodiky, které se zaměřují na flexibilitu. Provedení formální specifikace celého systému předem je často vnímáno jako opak flexibility. Existuje však určitý výzkum výhod používání formálních specifikací s „agilním“ vývojem
  • Složitost
    • K jejich efektivnímu pochopení a aplikaci vyžadují vysokou úroveň matematických znalostí a analytických dovedností
    • Řešením by bylo vyvinout nástroje a modely, které umožní implementaci těchto technik, ale skryjí základní matematiku
  • Omezený rozsah
    • Nezachycují vlastnosti zájmu pro všechny zúčastněné strany v projektu
    • Nedělají dobrou práci při určování uživatelských rozhraní a interakce s uživatelem
  • Není nákladově efektivní
    • To není úplně pravda, protože jejich použití je omezeno pouze na základní části kritických systémů, které se ukázaly jako nákladově efektivní

Další omezení:

  • Izolace
  • Ontologie nízké úrovně
  • Špatné vedení
  • Špatné oddělení obav
  • Špatná zpětná vazba nástroje

Paradigmata

Formální specifikační techniky existují v různých doménách a v různých měřítcích již nějakou dobu. Implementace formálních specifikací se bude lišit v závislosti na tom, jaký druh systému se pokoušejí modelovat, jak jsou aplikovány a v jakém bodě životního cyklu softwaru byly zavedeny. Tyto typy modelů lze kategorizovat do následujících paradigmat specifikací:

  • Specifikace založená na historii
    • chování založené na historii systému
    • tvrzení jsou interpretována v průběhu času
  • Specifikace založená na stavu
    • chování na základě stavů systému
    • řada postupných kroků (např. finanční transakce)
    • jazyky jako Z , VDM nebo B spoléhají na toto paradigma
  • Specifikace založená na přechodu
    • chování založené na přechodech ze stavu do stavu systému
    • nejlépe použít s reaktivním systémem
    • jazyky jako Statecharts, PROMELA, STeP-SPL, RSML nebo SCR spoléhají na toto paradigma
  • Funkční specifikace
    • určit systém jako strukturu matematických funkcí
    • OBJ, ASL, PLUSS, LARCH, HOL nebo PVS spoléhají na toto paradigma
  • Provozní specifikace
    • rané jazyky jako Paisley , GIST, Petriho sítě nebo procesní algebry spoléhají na toto paradigma

Kromě výše uvedených paradigmat existují způsoby, jak použít určitou heuristiku, aby se zlepšila tvorba těchto specifikací. Zde odkazovaný dokument nejlépe pojednává o heuristikách, které je třeba použít při navrhování specifikace. Činí tak použitím přístupu rozděl a panuj .

Softwarové nástroje

Zápis Z je příkladem předního formálního specifikačního jazyka . Mezi další patří Specifikační jazyk (VDM-SL) Vídeňské rozvojové metody a Abstrakt Machine Notation (AMN) B-metody . V oblasti webových služeb se k popisu nefunkčních vlastností ( kvalita služeb webových služeb ) často používá formální specifikace .

Některé nástroje jsou:

Příklady

Příklady implementace najdete v odkazech v části softwarové nástroje .

Viz také

Reference

externí odkazy