Předkládaný projekt se týká úvodních fází návrhu distribuovaných aplikací systémů založených na počítačových sítích. Cílem projektu je vytvoření rámce pro formální specifikace, verifikace a prototypování síťových aplikací, které zahrnou jak rozsáhlé informační systémy, tak i malé komponenty vestavěné např. do mobilních zařízení. Hlavní pozornost bude zaměřena jak na specifikace architektury, tak i reaktivního chování a chování v reálném čase užitím strukturovaného nebo objektově-orientovaného přístupu v závislosti na požadavcích aplikací. Cílem projektu nebude vyvíjet nový formální aparát, ale vytvořit metody a techniky, které umožní využít existující prosředky formálních specifikací v reálných aplikacích. Specifikované požadavky zahrnou bezpečnost (safety) a zabezpečení (security) aplikací včetně jejich vzájemných souvislostí. Znalostní podpora návrhu bude zaměřena na oblast opakovaného využití verifikovaných specifikací. Implementační a integrační fáze projektu poskytne pilotní verze technik a nástrojů pro konceptuální návrh založený na znalostech příslušné aplikační oblasti, pro specifikaci architektury navrhovaných systémů, pro specifikaci reaktivního chování systémů a funkce v reálném čase, a dále pro rychlé prototypování.

Description in English
The proposed project deals with front-end parts of networked, distributed system application designs. The project targets creation of a formal specification, verification and prototyping framework for network applications ranging from large information systems down to small components embedded e.g. in mobile devices. Main attention will be focused both on architectural and behavioral specifications of either reactive or real-time activities utilizing either structured or object-oriented approach depending on application requirements. The project is not striving to develop a new formal approach; instead, it should create methods and techniques that enable to utilize current formal specification means in real-world applications. Specified requirements would cover both safety and security of applications including their interrelations. Knowledge-based support will be focused on reuse of verified formal specifications. The implementation and integration phases of the project will provide pilot versions of techniques and tools for conceptual design stemming from application domain knowledge, for architectural specifications of designed systems, for reactive and real-time system behavior specifications, and for rapid prototyping.

Keywords
Formální specifikace, verifikace, rychlé prototypování, aplikace informačních systémů, komunikační protokoly

Key words in English
Formal specs, virifications, rapid prototyping, information system applications, communication protocols

GA102/05/0723

Czech

Švéda Miroslav, prof. Ing., CSc. - principal person responsible
Hruška Tomáš, prof. Ing., CSc. - fellow researcher
Matoušek Petr, doc. Ing., Ph.D., M.A. - fellow researcher
Ráb Jaroslav, Ing. - fellow researcher
Ščuglík František, Ing., Ph.D. - fellow researcher
Zendulka Jaroslav, doc. Ing., CSc. - fellow researcher

Department of Information Systems
- responsible department (1.1.1989 - not assigned)
Information and Database Systems Research Group
- internal (29.3.2004 - 31.12.2007)
NES@FIT - Networks and distributed systems research group
- internal (29.3.2004 - 31.12.2007)
Department of Information Systems
- co-beneficiary (29.3.2004 - 31.12.2007)

RYCHLÝ, M.; TICHÁ, P. A Tool for Supporting Feature-Driven Development. Preprint of the Proceedings of CEE-SET 2007. Poznań, Poland: 2007. p. 185-196.
Detail

MATOUŠEK, P. Symbolic Data Structures for Parametric Verification. Brno: Faculty of Information Technology BUT, 2005. p. 0-0.
Detail

HRUŠKA, T. DATAKON 2005 -Proceedings of the Annual Database Conference (ed. Tomáš Hruška). Brno: Masarykova universita, 2005. ISBN: 80-210-3813-6.
Detail

MATOUŠEK, P. Nástroje pro analýzu bezpečnostních protokolů. Brno: 2006. p. 0-0.
Detail

ZENDULKA, J. Proceedings of 8th Spring International Conference ISIM'05. Ostrava: Marq software s.r.o., 2005. p. 0-0. ISBN: 80-86840-09-02.
Detail

MATOUŠEK, P. Praktické úlohy z počítačových sítí. Brno: 2006. s. 0-0.
Detail

RYŠAVÝ, O. Inheritance of specifications in the calculus of functional objects. Brno: Faculty of Information Technology BUT, 2006.
Detail

ŠVÉDA, M.; VRBA, R. Embedded Systems with IEEE 1451.1 on Internet. In Enabling Technologies for the New Knowledge Society. Cairo: IEEE Computer Society, 2005. p. 539-550. ISBN: 0-7803-9270-1.
Detail

OČENÁŠEK, P.; TOUFAROVÁ, J. Zpřístupnění obsahu Internetu zrakově handicapovaným uživatelům. INFORUM 2005: 11. ročník konference o profesionálních informačních zdrojích, 2005, roč. 2005, č. 1, s. 1-8. ISSN: 1801-2213.
Detail

MATOUŠEK, P. Kombinované rešení switch/router. Journal CONNECT!, 2007, roč. 2007, č. 4, s. 40-41. ISSN: 1211-3085.
Detail

OČENÁŠEK, P.; TRCHALÍK, R. On the Implementation of Metrics in the Workflow System. WSEAS Transactions on Computers Research, 2006, vol. 1, no. 2, p. 360-362. ISSN: 1991-8755.
Detail

OČENÁŠEK, P. Automatic System for Making Web Content Accessible for Visually Impaired Users. WSEAS Transactions on Computers Research, 2006, vol. 1, no. 2, p. 325-328. ISSN: 1991-8755.
Detail

MATOUŠEK, P. Dobrého nespálí - test firewallů pro sítě do 150 uživatelů. Journal CONNECT!, 2006, roč. 2006, č. 6, s. 26-29. ISSN: 1211-3085.
Detail

MATOUŠEK, P. Není datům v síti těsno?. Journal CONNECT!, 2005, roč. 2005, č. 11, s. 7-8. ISSN: 1211-3085.
Detail

ŠČUGLÍK, F. Time Synchronization Possibilities in Wireless networks for Embedded Systems. WSEAS TRANSACTIONS on COMMUNICATIONS, 2005, vol. 4, no. 11, p. 1215-1219. ISSN: 1109-2742.
Detail

ŠČUGLÍK, F. Relation between UML2 Activity Diagrams and CSP algebra. WSEAS Transactions on Computers, 2005, vol. 4, no. 10, p. 1234-1240. ISSN: 1109-2750.
Detail

BURGETOVÁ, I.; ZENDULKA, J. Clustering of Protein Sequences. Proceedings of 1st International Workshop WFM'06. Přerov: Marq software s.r.o., 2006. p. 71-78. ISBN: 80-86840-20-4.
Detail

SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z. Verifying VHDL Design with Multiple Clocks in SMV. In Formal Methods: Applications and Technology. Lecture Notes in Computer Science. Lecture Notes in Computer Science 4346. Bonn: Springer Verlag, 2007. p. 148-164. ISBN: 978-3-540-70951-0. ISSN: 0302-9743.
Detail

MATOUŠEK, P.; SMRČKA, A.; VOJNAR, T. High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science. Lecture Notes in Computer Science 3725/2005. Berlin: Springer Verlag, 2005. p. 371-375. ISBN: 978-3-540-29105-3. ISSN: 0302-9743.
Detail

OČENÁŠEK, P. Tools for Analysis and Simulation of Protocol Communication. EDS '07 IMAPS CS International Conference Proceedings. Brno: Brno University of Technology, 2007. p. 87-91. ISBN: 978-80-214-3470-7.
Detail

Responsibility: Švéda Miroslav, prof. Ing., CSc.