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.

Description in English
The project focuses on object-oriented techniques for development and specification of computer systems. Currently, the most used industrial techniques of this area is UML. The UML provides a set of diagrams for support of analyzing and modeling various aspects of computer systems. Nevertheless, a lack of formally defined semantics has invited several group of researches to attempt providing a suitable formal basis. The proposed project aims at selecting of currently available formal tools and theories for formal specification and developing of a formal theory interpreting of the UML meta-layer definitions to provide a formal foundation for the UML semantics.

Keywords
formální specifikace, objektový návrh a modelování, UML, formální dokazování, logiky vyššího řádu

Key words in English
formal specification, object oriented design and modelling, UML, theorem proving, higher-order logics

FR838/2003/G1

Czech

Ryšavý Ondřej, doc. Ing., Ph.D. - principal person responsible

Responsibility: Ryšavý Ondřej, doc. Ing., Ph.D.