Projects

Project name	Project description
European Research Network on Formal Proofs	If testing can reveal errors in computer programs, only formal verification can guarantee their absence. The highest Evaluation Assurance Levels of the Common Criteria for Information Technology Security Evaluation require automatically checked mathematical proofs of correctness. Proofs are also the basis of mathematics and many sciences, and thus are very important in education and research. In many computer technologies, developers and users rely on standard languages and protocols for exchanging data and enabling tool interoperability: TCP/IP for network communication, HTML for web pages, etc. This is however not the case for formal proofs, which is a major bottleneck for their adoption by the industry. The main reason is that, currently, proof systems use mutually incompatible logical foundations. Fortunately, only small parts of the proofs developed in a system use features that are incompatible with other systems. Europe is a leading actor in the area of formal proofs: about 65% of the proof systems of the world are developed in Europe, including the two most used proof assistants, Coq and Isabelle. This Action aims at boosting the interoperability and usability of proof systems and making formal proofs enter a new era. For the first time, it gathers all the developers and users of proof systems in Europe. To make the proofs exchangeable, they will express, in a common logical framework, the logical foundations of their systems and develop tools for inter-translation of the proofs developed in individual systems to and from this common logical framework.
Promoting Sustainability as a Fundamental Driver in Software Development Training and Education
Interactive pattern-driven language development	The goal of this project is to explore novel approaches to formal language design and implementation. They should be based on synthesis of methods from the fields of formal languages, human-computer interaction and data analysis. Language design and implementation process should be interactive and explorative activity, where language designer is able to experiment with design of the language notation and associated tools and immediately adjust language definition based on the results. To achieve this it would be required to design new methods for automated inference of language specification based on abstract syntax, example sentences and interaction with language designer.
Semantic Modeling of Component-Based Program Systems	The main goal of this project is to investigate the construction and behavior of component-based systems to ensure their reliability and desired behavior. To ensure the reliable execution of a complex program system composed of components, not only its static construction but also its dynamic behavior plays an important role. Thus the meaning of the basic concepts has to be precisely understood and rigorous rules have to be followed. However, while the construction of component-based program systems is well described in various publications with respect to practical aspects for working programmers, only a few publications define the construction of component-based systems formally. This research is based on the expertise of the Slovak partner on the categorical semantics of programs, on the expertise of the Austrian partner on logical system modeling and analysis, and on the fruitful cooperation of both partners in a previous collaboration project.
Setting the trends in IoT education	This project addresses the development of skills involving the emerging Internet of Things (IoT) (also known as Industry 4.0) technologies. The main focus falls on training, teaching and learning activities that better prepare the future IoT educators and instructors at the vocational and higher educational levels, and also indirectly, the users/developers/entrepreneurs/innovators that will shape the future of IoT. The project focuses on the development of core educational materials and of an open online community to consume, share, review and enhance these materials. This will ensure a dynamic IoT educational platform where persons interested in this field will interact directly.
Manufacturing Industry Digital Innovation Hubs	MIDIH "Manufacturing Industry Digital Innovation Hubs", is a "one stop shop" of services, providing industry with access to the most advanced digital solutions, the most advanced industrial experiments, pools of human and industrial competencies and access to "ICT for Manufacturing" market and financial opportunities. MIDIHs will leverage networks of local Competence Centres, each specialised in peculiar aspects of the CPPS/IIOT (Cyber Physical Production System / Industrial Internet of Things) technologies and able to attract, mentor and nurture local Manufacturing SMEs towards Industry 4.0 projects, experiments and business. A common platform of knowledge, methods and collaboration tools will be shared among the MIDIHs network and allow cross-border fertilisation, continuous improvement, open innovation.
Návrh a vývoj verifikovateľnej BDI architektúry pre IDS s využitím komponentových systémov a systémov virtuálnej reality	V súčasnej informačnej spoločnosti je počítačová bezpečnosť nesporne veľmi aktuálnou oblasťou výskumu. V tejto oblasti musí byť obzvlášť kladený dôraz na návrh a vývoj spoľahlivých a bezpečných programových systémov. Jednou z možností ich vývoja je využitie komponentových systémov. V tomto projekte rozšírime pasívnu rolu IDS na aktívnu (t.j. automatizované reakcie systému na detegované sieťové narušenie). Na to využijeme inteligentnú BDI architektúru, ktorú navrhneme pre naše účely. Pri návrhu takejto architektúry musí byť obzvlášť kladený dôraz na jej korektnosť a spoľahlivosť. To bude zaručené využitím vhodných verifikačných formálnych metód. Navrhnutú architektúru implementujeme ako komponentový systém, kde jednotlivé komponenty budú predstavovať funkčné jednotky BDI architektúry. Ďalším cieľom bude vytvorenie vhodného používateľského rozhrania prostredníctvom systémov virtuálnej reality kvôli empirickému overovaniu práce s navrhnutým systémom.
Enhancing cognition and motor rehabilitation using mixed reality	Technological advancements based on mixed reality (MR) offer various challenges for research and medical treatment. The project focuses on two objectives related to healthy subjects and hemiparetic patients after stroke. First, we will test the hypothesis whether cognitive training using appropriately designed MR environment will enhance perceptual and cognitive performance in healthy subjects. This will be tested by computerized psychological experiments as well as by measuring event-related potentials or ERPs. Second, we will test the hypothesis whether experience with training in MR (in combination with motor-imagery based brain-computer interface developed by us) will enhance oscillatory sensory-motor rhythms. This will be tested by measuring subject’s EEG activity before and after each training session, clinical testing, as well as by the questionnaires aiming to learn about human factors including mental fatigue, motivation, irritation or sleepiness due to training. In both objectives, we will design and implement a set of testing procedures, carry out a battery of dedicated experiments, and critically evaluate the results with the goal to validate MR designs.
Intelligent Dynamic Spectrum Access Management for the Future Cognitive Communication Networks	Hlavná technologická výzva sprevádzaná 5. generáciu mobilných komunikačných systémov je efektívne využitie dostupného frekvenčného spektra. Statické prideľovania frekvenčného spektra sa javí ako nedostatočné a jedno z možných riešení tohto problému je dynamické prideľovanie spektra pri použití technológie kognitívneho rádia. Technológia kognitívneho rádia je v súčasnosti mimoriadne diskutovaná oblasť, v ktorej sa otvára celé spektrum vyšetrovaných tém. Dynamické pridelovanie spektra je možné považovat za jednu z najvýznamnejších. Za základne funkčné bloky kognitívneho rádia je možné označiť blok monitorovania spektra, blok distribúcie a zdieľania spektra a nakoniec ekonomický blok distribúcie spektra. Súčasný stav poznania v oblasti dynamického prideľovania spektra sa výrazne limituje na analýzu vyšetrovania prevádzkových vlastností jednotlivých blokov, avšak ich vzájomná optimalizácia v dôsledku vysokej komplexity kognitívnej rádiovej siete je často obchádzaná. S cieľom riešiť tento problém, bude projekt IDR-KKS zameraný na vzájomnú optimalizáciu prevádzkových parametrov monitorovania a zdieľania spektra a ich dopad na navrhnuté ekonomické modely uvažovaných bezdrôtových štandardov 5G. Za účelom zachytenia vysokej dynamiky kognitívnej rádiovej siete, budeme v rámci projektu IDR-KKS uvažovať agentový prístup k modelovaniu a simulácií, ktorý sa ukázal ako veľmi efektívny v iných vedných odboroch (fyzika, ekonómia). Efektívnosť navrhnutých agentových modelov bude verifikovaná podľa vhodne zvolených scenárov. V rámci projektu IDR-KKS bude tiež realizovaná experimentálna kognitívna rádiová sieť umožňujúca verifikovať agentové modely aj v reálnej prevádzke.
Implementation of Modern Methods and Education Forms in the Area of Security of Information and Communication Technologies towards Requirements of Labour Market	The increasing development of information society and its globalization is growing proportionally with the need to appropriately secure information and communication technologies. In this context, in the area of computer security there is an increasing demand for highly qualified professionals, where the current demand exceeds the offers of the labor market. Such a disproportion exerts high requirements on education in the area of security of particular university study programs. In order to successfully handle such a task, it is necessary to consider specialized university courses within the educational process along with an arising need for a close relation between particular courses of the study program. It may be expected that the deepening of the mutual relation between Informatics courses and the computer and software engineering, regarding security issues of the ICT (Information and Communication Technologies), will result in the increased quality of student preparation of the Informatics program. This is why the strategic goal of this project is to search for new methods, forms and technologies to transfer knowledge from the area of security to courses of the other study programs, using a suitable platform towards strategic requirements of the labor market. The solution will be implemented regarding the main goals, namely the innovation of the study Informatics program at the DCCI FEEI TUKE towards the issues of the ICT security, technical ensuring of the new education form in selected courses, and the creation of guides and examples for a practical application of the security knowledge towards the other courses. Students will be able to implement pragmatic project tasks, defined by the corresponding course, with a practical usethe result. As expected by the research team, this will have a positive impact on the quality of the education in the Informatics study program.