Faculty, PhD students, and Red Hat associates in the Czech Republic are collaborating actively on the following research projects. This quarter we once again highlight collaborative projects at Masaryk University (Brno), Brno University of Technology, and Czech Technical University (Prague). We will highlight research collaborations from other parts of the world in future editions of the Red Hat Research Quarterly. Contact academic@redhat.com for more information on any project.
PROJECT: AUFOVER (Automated Formal Verification)
Academic investigators: Honeywell: Mgr. Tomáš Kratochvíla; Paradise: Prof. RNDr. Jiří Barnat, PhD; Formela: Doc. RNDr. Jan Strejček, PhD; VeriFIT: Prof. Ing. Tomáš Vojnar, PhD, and Ing. Aleš Smrčka, PhD
Red Hat investigators: Kamil Dudka and Ondřej Vašík
In 2019, we offered Symbiotic and Divine as RPM packages and developed utilities to convert their output into a unified, machine-readable format. We then started to see unexpected changes in the output of formal verification tools as the tools are updated. This observation drove us to create our own test suite, named aufover-benchmark, where multiple tools are exercised by the same set of tests. This in turn helped us discover previously unknown bugs in the formal verification tools. These bugs were reported to developers of the tools, and many of them have been fixed.
Now we are moving the automation to the next level. Our ultimate goal is to run formal verification tools on unmodified source RPM packages. Unlike static analyzers, where we instrument only compilation of the source code, we now need to instrument the execution of binaries produced by the build in addition.
At the same time, we want to interfere with the testing frameworks used by RPM packages as little as possible. To tackle this problem, we developed csexec—a dynamic linker wrapper. The wrapper can be used as an ELF interpreter while linking binaries during the build of RPM packages. Then we can transparently choose which formal verification tool should be used to instrument execution of the binaries while running test suites embedded in source RPM packages. Although the original motivation for developing csexec was to run formal verification tools, the wrapper can easily be used to run dynamic analyzers (such as valgrind or strace) on unmodified RPM packages, as shown in the following quick demo: https://github.com/kdudka/cswrap/wiki/csexec
PROJECT: PatrIOT—IoT Testing Framework
Academic investigators: Miroslav Bureš
Red Hat investigators: Štefan Bunčiak and Miroslav Jaroš
PatrIOT has resulted in three submitted US patents by Red Hat and three submitted CZ patents by FEE CTU (Faculty of Electrical Engineering, Czech Technical University). This project is pushing state-of-the-art borders in several R&D areas. As the IoT industry is growing, the project has hit perfect timing to fill the market gap in the field of IoT testing. The testing framework was very well received on the market by important enterprises—namely, Skoda Auto, Rockwell, Siemens, and Electrolux—who provided positive feedback. The grant for this project from TACR (Technology Agency of the Czech Republic) ended in 2020, but the project now continues as self-funded until the next call for grant applications.
PROJECT: Innovation Scorecard
Academic investigators: doc. Ing. Ondřej Žižlavský, PhD, Eddie Fisher, and Tetyana Shpilka
Red Hat investigators: Marcel Gazdík, Vojtěch Sokol, and Tomáš Meszároš
Innovation Scorecard, originating at the Faculty of Business, was a rather unconventional project for a Red Hat partnership. Prior to this project, Red Hat Czech was mostly concentrating on cooperation with faculties focused on computer science. This project provides a methodology to drive innovation in project management. In 2018 it was funded by TACR for three years. After two years of working with multiple teams in Brno, a lot of case data has accumulated, resulting in publications and mentions by the Project Management Institute (PMI). Innovation Scorecard is now heading into its third year with Red Hat, and its creators are planning to publish an ebook with the certified methodology.
PROJECT: Vega Project
Academic investigators: Gabriel Szász
Red Hat investigators: Nikolaos Moraitis, Zdeněk Švécar, and Filip Hubík
The project is using OpenShift as a platform for execution and monitoring of scientific computations. An OpenShift-based framework supports scalable parallel open hybrid computing and enables easier distribution, scalability, and flexibility of already-written code that cannot be compiled on a supercomputer or parallelized otherwise. In addition, the decomposition of a complex pipeline into simpler subunits provides better maintainability and simplifies debugging. The project is currently challenged by lack of resources. Options for providing more hardware (and thus computing power) are being explored to allow the project to move forward.