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

Název anglicky

Tools for support of formal specification and verification of UML based diagrams

Typ

grant

Klíčová slova

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

Abstrakt

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.

Řešitelé

Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT) , hlavní řešitel
Dvořák Václav, prof. Ing., DrSc. (UPSY FIT VUT) , spoluřešitel

Publikace

2004

BUREŠ František a RYŠAVÝ Ondřej. A Graph Representation for Use Case Specifications. In: Proceedings of the WSEAS International Conferences. Salzburg: World Scientific and Engineering Academy, 2004, s. 5. ISBN 960-8052-95-5. Detail
RYŠAVÝ Ondřej a BUREŠ František. A Graph Representation for Use Case Specifications. WSEAS Transactions on Computers, roč. 2004, č. 3, s. 686-690. ISSN 1109-2750. Detail

2003

RYŠAVÝ Ondřej a ŠVÉDA Miroslav. A Minimal Formal Language for Object-Oriented Specifications. In: Proceedings of the IEEE TC-ECBS and IFIP WG10.1 Joint Workshop on Formal Specifications of Computer-Based Systems, 2003. Huntsville, AL: University of Stirling, 2003, s. 35-40. ISBN 1-85769-189X. Detail
RYŠAVÝ Ondřej. A Survey on Formal Representation of UML. Brno, 2003. Detail
BUREŠ František a RYŠAVÝ Ondřej. Declarative Behaviour Description of Selected Class from Standard IEEE 1451.1. ElectronicsLetters.com, roč. 2003, č. 6, s. 6. ISSN 1213-161X. Detail
BUREŠ František a RYŠAVÝ Ondřej. Formal specification of IEEE1451.1 fragments. In: 11. International Conference on Software, Telecommunications & Computer Networks. Split: Faculty of Electrical Engineering, Mechanical Engineering and Naval Architecture , University of Split, 2003, s. 282-287. ISBN 953-6114-64-X. Detail
ŠČUGLÍK František. Visualizing formal specifications using diagrams. In: 11. International Conference on Software, Telecommunications & Computer Networks. Split: Faculty of Electrical Engineering, Mechanical Engineering and Naval Architecture , University of Split, 2003, s. 5. ISBN 953-6114-64-X. Detail