to top
Select language:    en ENGLISH  |  cs CZECH
Polyspace Code Prover
picture
Prokázání absence run-time chyb v software
Hlavním cílem nasazení nástroje Polyspace Code Prover je prokázání absence přetečení, dělení nulou, indexování za hranicemi pole a dalších run-time chyb ve zdrojovém kódu v jazyce C a C++. Nástroj využívá statické analýzy a abstraktní interpretace založené na formálních metodách. Prokazuje tak spolehlivost kódu bez nutnosti spuštění programu nebo tvorby testovacích příkladů. Lze ověřovat ručně psaný kód, automaticky generovaný kód nebo jejich kombinaci. Každá operace v prověřovaném kódu je barevně označena podle toho, zda prokazatelně nezpůsobí run-time chybu, je prokázáno selhání, jedná se o nedosažitelnou část kódu nebo zda není možné prokázat absenci chyby.
Polyspace Code Prover také zobrazuje množství informací o proměnných a návratových hodnotách funkcí a může prokazatelně určit podmínky, za kterých proměnné překročí meze daného rozsahu hodnot. Nástroj umožní i sledování metrik charakterizujících kvalitu kódu, které lze využít ke splnění stanovených kritérií na kvalitu softwaru. Polyspace Code Prover lze integrovat do buildovacích systémů za účelem automatického prověřování kódu.
Jak na to
eBook zdarma
WWW semináře CZ/SK
User Stories
Nejbližší plánované akce:

© HUMUSOFT 1991 - 2019