|
Návrh a testování softwaru pro systémy s vysokými nároky na bezpečnost a spolehlivost
Článek se věnuje problematice vývoje softwaru pro reaktivní systémy, které se užívají v řídicích systémech. Tyto systémy lze obvykle popsat jednoduchým matematickým modelem, což umožňuje automatizovat důkaz správnosti jejich návrhu i testování jejich implementace.
1. Úvod
Při vývoji systémů s vysokými nároky na bezpečnost a spolehlivost jsou kladeny přísné požadavky na jejich přesnou specifikaci a důkladné testování. Matematický popis systému umožní jak simulaci či automatické generování kódu, tak provedení matematického důkazu správnosti a bezespornosti specifikace. Model systému lze také využít při generování testovacích sekvencí. Ačkoliv je vytvoření formální specifikace nákladné, lze formalizací problému předejít mnoha chybám ve specifikaci a implementaci, které by mohly výrazně zvyšovat výsledné náklady na vývoj systému. Navíc může ověřenou formální specifikaci použít nezávislý validátor jako cenný podklad pro své rozhodování o bezpečnosti vyvinutého systému.
V následujících kapitolách čtenářům nejprve přiblížíme vlastnosti diskutovaných systémů. Dále vysvětlíme, jakým způsobem lze automatizovaně verifikovat návrh systému. Na konci příspěvku je diskutována problematika testování implementace systému.
2. Reaktivní systémy
Softwarové systémy lze rozdělit na tři druhy [5]:
Transformační systémy ukončí svoji činnost, je-li vygenerován výsledek podle zadaného vstupu. Jsou to např. kompilátory.
Interaktivní systémy komunikují se svým okolím svou vlastní rychlostí (okolí na ně musí čekat). Jsou to např. paralelní procesy v běžných operačních systémech, databázové či webové servery apod.
Reaktivní systémy reagují na okolí, které na ně nemůže čekat. Jsou to např. řídicí systémy fyzikálních procesů. Oproti interaktivním systémům je u nich požadována deterministická vstupně-výstupní i časová odezva.
Reaktivní systémy je obvykle vhodné modelovat jako paralelní složení jednodušších procesů a jejich okolí (obr. 1). Z hlediska komunikace je lze dále rozdělit na synchronní a asynchronní. Oba případy se většinou popisují konečným automatem (nejčastěji Mealyho automatem).
Díky jednoduchosti výpočetního modelu konečných automatů lze při vývoji reaktivních systémů kombinovat metody pro specifikaci, verifikaci a testování hardwaru a softwaru.
3. Verifikace návrhu systému
Úkolem verifikace je ověřit správnost návrhu systému. K tomu je třeba popsat vyvíjený systém v určitém jazyce s přesně definovanou syntaxí a sémantikou. Důležité je také vyjádřit požadované vlastnosti systému, např.:
- v systému nemůže nastat mrtvý stav – deadlock (deadlock freedom),
- systém se nikdy nedostane do špatného stavu (safety properties),
- systém vždy může přejít do správného stavu (liveness properties).
Požadované vlastnosti lze vyjádřit buď jako formuli ve zvolené logice (např. v temporální logice CTL [4]) nebo jako pozorovatel [5], tj. jako procesy indikující správnost odezvy vyvíjeného systému. Tyto procesy jsou k systému připojeny paralelně, viz obr. 2. Výhodou pozorovatelů je, že jsou popsány ve stejném jazyce jako navrhovaný systém a není třeba rozumět logickým formulím.
Existuje-li formální model systému (program ve vybraném jazyce) a formálně vyjádřené požadované vlastnosti, je možné přistoupit k verifikaci specifikace. Jde vlastně o provedení důkazu, že model systému splňuje požadované vlastnosti. Takový důkaz lze obecně provést dedukčním systémem s přepisovacími pravidly [2]. K ověření vlastností konečných automatů je ale možné použít i plně automatizované nástroje založené na přístupu zvaném model-checking.
3.1 Model-checking
Model-checking [3] byl úspěšně aplikován v mnoha úlohách v praxi, např. při návrhu hardwaru, analýze komunikačních protokolů, reaktivních systémů atd. Je založen na „chytrém“ prohledávání (konečného) stavového prostoru a ověřování, že daná vlastnost je splněna. Není-li ověřovaná vlastnost splněna, poskytne metoda protipříklad, který ukáže cestu (sekvenci vstupů) z počátečního stavu do stavu, kde došlo k porušení zkoumané vlastnosti.
Pro přiblížení principu uveďme hlavní myšlenky metody „symbolický model-checking“:
- Systém (konečný automat) je reprezentován počátečním stavem I(s) a přechodovou funkcí T(s, a, s’) ve formě logických formulí, kde s jsou stavové proměnné, a vstupní proměnné a s’ jsou proměnné reprezentující následující stav.
- Množiny stavů jsou reprezentovány jako logické formule nad proměnnými s, a a s’. Množinové operace nad stavy jsou tak transformovány na logické operace nad formulemi.
- Používají se efektivní algoritmy pro práci se speciální reprezentací logických formulí, např. v podobě BDD (Binary Decision Diagram), BED (Boolean Expression Diagram) atd. (obr. 3).
- Vlastnosti systému jsou vyjádřeny v temporální logice, např. CTL.
- Pro práci s vlastnostmi v temporální logice a pro výpočet stavů dosažitelných z počátečního stavu je důležitá funkce image, která vrací množinu stavů dosažitelných přechody T z výchozí množiny R. Inverzní funkce preimage vrací výchozí množinu stavů, ze které se přechody T dostanou do stavů R.
- Protože je modelovaný systém konečný, důkaz vlastnosti vždy skončí. Buď je vlastnost splněna, nebo je vrácen protipříklad (pokud existuje).
Nevýhodou metody model-checking je nebezpečí stavové exploze, kdy s rostoucí velikostí systémů (počtem vstupů, výstupů a stavů) neúměrně narůstá počet analyzovaných stavů. V současné době lze automaticky verifikovat systémy do velikosti kolem stovek až tisíců logických proměnných (vstupů, výstupů a stavů). Některé nástroje umějí pracovat i s jinými typy proměnných, než jsou logické, např. s celými či reálnými čísly, a s podmínkami v podobě lineárních omezení.
4. Testování implementace
Vytvoření a ověření formální specifikace však nemůže nahradit testování systému, kde se mohou projevit nepředvídané vlivy, které v abstraktním modelu systému nebyly brány v úvahu. Testování zůstává důležitou komplementární činností, kterou lze na základě formální specifikace automatizovat. Obecně lze ale říci, že kvalitní systém se získá vhodným návrhem, a ne testováním. Testování může „pouze“ ukázat, že produkt je špatný, ne že je dobrý. Navíc je mnohem úspornější detekovat chyby v počátečních stadiích vývoje systému.
V dalším textu se zaměříme na metody testování shody specifikace a implementace zvané conformance testing. Jde o testování „black-box“, kdy tester nemá přístup ke zdrojovému kódu. Cílem takového testování reaktivního systému je ukázat, že všechny stavy a přechody jsou správně implementovány.
Proces testování sestává z vytvoření testovacího systému a testovacích sekvencí. Vytvořit testovací systém nebývá problém. Nejtěžší je nalézt testovací sekvence, které by testovaly chování implementace vyvinutého systému. V průmyslové praxi je vhodné generování testovacích sekvencí automatizovat, neboť napsání sady testovacích sekvencí zabírá mnoho času a člověk je schopen pracovat jen s problémy limitované velikosti. Různé testovací metody lze hodnotit podle těchto kritérií:
- Schopnost detekce chyb. U konečných automatů se rozlišují tři druhy chyb: chyba výstupu; chyba přechodu; chyba výstupu i přechodu.
- Délka testovací sekvence.
- Použitelnost. Při vytváření testovací sady je snaha maximalizovat schopnost detekce chyb a zároveň minimalizovat velikost této sady.
Dále lze testovací metody hodnotit podle toho, zda systém testují vyčerpávajícím způsobem nebo jen částečně.
4.1 Testování malých systémů
Malé systémy lze testovat vyčerpávajícím způsobem. Testovací sekvence se pak skládají z několika částí (obr. 4):
Startovací sekvence dostane testovaný systém z počátečního stavu systému do počátečního stavu testovaného přechodu.
Provede se testovaný přechod.
Jestliže to konkrétní metoda umožňuje, hledají se skryté stavy až do maximální definované hloubky. Skryté stavy jsou takové, které není možné na základě pozorování rozlišit od jiných stavů. Existence takových skrytých stavů se nemusí během testování projevit. Může se projevit pouze výjimečně (např. zdánlivě náhodnou chybou při přetečení nějakého čítače), což ale může mít v případě reaktivních systémů nedozírné následky. Při hledání skrytých stavů lze pouze přijmout předpoklad, že testovaný systém jich má omezený počet.
Ověří se, zda se systém dostal testovaným přechodem do požadovaného stavu. Toto ověření se provádí aplikací rozlišovacích sekvencí, které od sebe odliší různé stavy.
Aplikuje se sekvence vstupů, která vrátí testovaný systém zpět do počátečního stavu.
Pro přiblížení zmiňme dvě základní metody, které systémy testují vyčerpávajícím způsobem [6]:
Cesta všemi přechody (transition tour) je sekvence přechodů, která začíná v počátečním stavu systému, projde všechny přechody konečného automatu alespoň jednou a vrátí se zpět do výchozího stavu. Nalezení optimální sekvence lze formulovat jako tzv. problém čínského listonoše1). Tato metoda detekuje všechny chyby výstupu, ale nezjistí chyby v přechodové funkci konečného automatu.
W-metoda používá dvě množiny sekvencí. W-set je množina sekvencí, které od sebe rozliší každé dva stavy (obr. 5). P-set je množina sekvencí, které převedou systém do všech požadovaných stavů. Testovací sekvence vzniknou spojením sekvencí z množin P-set a W-set. Tato metoda má vysokou detekční schopnost chyb a navíc umožňuje hledat skryté stavy.
4.2 Testování rozsáhlých systémů
Testování s průvodcem (guided testing). Proces testování je řízen člověkem, který vybírá cíle (stavy, přechody), jejichž testováním se zvýší zvolená míra pokrytí (stavů, přechodů, chyb) testovací sady. Testování může být automatizováno využitím plánovačů, které vyhledávají sekvenci vstupů převádějící testovaný systém z výchozího do cílového stavu.
Mutační analýza. Z modelu systému se jednoduchými syntaktickými změnami vytvářejí „mutované“ programy. Cílem testeru je vytvořit takové testovací sekvence, které rozliší vytvořený mutant od původního modelu [7].
Popsané metody jsou nepoužitelné pro testování velkých systémů. V takovém případě lze užít částečné testovací metody, jako např.:
Obě již zmíněné metody lze s výhodou automatizovat při použití metod procházení stavového prostoru známých z metody model-checking.
5. Závěr
Při vývoji systémů s vysokými nároky na bezpečnost a spolehlivost jsou evropskými normami kladeny vysoké nároky na řádnou specifikaci systému, verifikaci správnosti návrhu a důkladné testování systému. Použití formálních metod umožňuje tyto problémy do značné míry systematizovat a automatizovat. Nevýhodou jsou však vysoké náklady na tvorbu formální specifikace a nároky na kvalifikaci pracovníků vývoje. V praxi se proto identifikují jen ty nejkritičtější části systému, které se pak vyvíjejí pomocí již popsaných metod.
Jako příklad zmiňme Elektronický automatický blok ABE-1, vyvinutý firmou AŽD Praha, s. r. o., který získal na MSV 2001 zlatou medaili (viz Automa 12/2001) a na jehož vývoji se katedra kybernetiky ČVUT FEL aktivně podílela [1], [2].
Literatura:
[1] HLAVATÝ, T. – PŘEUČIL, L.: Formal Methods in Development and Testing of Safety-Critical Applications. In: Proceedings Process Control – ŘIP 2002. University of Pardubice, Pardubice, 2002, vol. 1, p. 104. ISBN 80-7194--452-1.
[2] ŠTĚPÁN, P. – PŘEUČIL, L.: Methods for improving software quality. In: Proceedings of International Carpathian Control Conference. TU FEI Košice. Košice, 2000. Vol. 1, pp. 665–668.
[3] McMILLAN, K. L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell, Massachusetts, 1993.
[4] CLARKE, E. M. – EMERSON, E. A. – SISTLA, A. P.: Automatic verification of finite state concurrent systems using temporal logic specifications. A practical approach. In: Symposium on Principles of Programming Languages, 1983, pp. 117–126.
[5] HALBWACHS, N. – LAGNIER, F. – RATEL, C: Programming and verifying real-time systems by means of the synchronous data-flow programming language Lustre. In: IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, September 1992.
[6] LEE, D. – YANNAKAKIS, M.: Principles and methods of testing finite state machines – A survey. In: Proceedings of the IEEE, 1996, vol. 84, pp. 1090–1126.
[7] BANKS, D. – DASHIELL, W. – GALLAGHER, L. a kol.: Software testing by statistical methods–preliminary success estimates for approaches based on binomial models, coverage designs, mutation testing and usage models. Technical Report NISTIR 6129, National Institute of Standards and Technology (NIST), Gaithersburg, MD., March 12 1998.
Ing. Tomáš Hlavatý,
katedra kybernetiky ČVUT FEL
(hlavaty@labe.felk.cvut.cz)
|