Nástroje pro podporu formální specifikace a verifikace UML diagramů

Navrhovaný projekt je zaměřen na oblast návrhu a specifikace softwarového vybavení pomocí objektově orientovaných modelovacích technik. V současné době je nejpoužívanějším modelovacím jazykem UML. Tento jazyk poskytuje prostřednictvím svých diagramů základ pro modelování a analýzu nejrůznějších typů aplikací v nejrůznějších oblastech. Jeho univerzálnost však způsobuje, že lze vytvářet modely postrádající přesný formálně jednoznačný význam, který je nutný k tomu, aby mohl být navrhovaný systém podroben procesu automatického ověřování jeho vlastností. Tento nedostatek si uvědomují i samotní tvůrci jazyka UML a bylo založeno několik skupin, které se zabývají tvorbou jednoznačné sémantiky jednotlivých částí jazyka UML. Vytvoření přesných sémantických modelů se stane základem pro množinu transformačních pravidel, které umožní vytvoření dedukčního systému nad jednotlivými diagramy UML. Jelikož tyto pravidla leží na úrovni metajazyku UML nebude nežádoucím výsledkem zpřesnění UML jeho složitější notace. Navržený projekt si klade za cíl upravit a doplnit stávající nástroje pro formální specifikaci a verifikaci, tak aby byly vhodným základem dedukčního systému UML. Nejpravděpodobnějším kandidátem je systém PVS. Jedná se o volně šiřitelný teorem prover, jehož specifikační jazyk tvoří silně typovaná logika vyššího řádu.