Each quarter, Red Hat Research Quarterly highlights new and ongoing research collaborations from around the world. This quarter we highlight collaborative projects in the Czech Republic, at Masaryk University (Brno), Brno University of Technology, and Czech Technical University (Prague).
Contact academic@redhat.com for more information on any project described here, or visit the Red Hat Research Project Directory on our website.
PROJECT: AUFOVER (Automated Formal Verification)
Academic investigators: Honeywell: Mgr. Tomáš Kratochvíla (Masaryk); Paradise: Prof. RNDr. Jiří Barnat, PhD (Masaryk); Formela: Doc. RNDr. Jan Strejček, PhD (Masaryk); VeriFIT: Prof. Ing. Tomáš Vojnar, PhD (BUT), and Ing. Aleš Smrčka, PhD (BUT)
Red Hat investigators: Kamil Dudka and Ondřej Vašík
At DevConf 2021, we presented our innovative solution to fully automatic dynamic analysis of unmodified source RPM packages. The solution was based on csexec, which is a wrapper of the system’s dynamic linker. Now we are extending this solution for select formal verification tools, namely CBMC, Divine, and Symbiotic.
Thanks to our experimental csmock plug-ins, developers can easily evaluate these tools on a given source RPM package by running a single command in their terminal. Although we are not able to complete the formal verification for the majority of Fedora RPM packages, the csmock plug-ins are optimized to deliver at least partial results in a predictable amount of time.
We are still working with developers of the formal verification tools to make their output format easier to understand by developers. We have provided patches to record and report the names of binaries executed, command line arguments passed to these binaries, and absolute paths to files containing the source code.
In our test suite, multiple tools are exercised by the same set of tests to help us discover bugs in the formal verification tools themselves. Called aufover-benchmark, the suite is now available in a public git repository and covered by a publicly available continuous integration (CI) system. All projects developed as part of the AUFOVER project are now consolidated under a single namespace in Github (github.com/aufover) and Fedora COPR (copr.fedorainfracloud.org/groups/g/aufover/coprs).
PROJECT: Innovation Scorecard
Academic investigators: Doc. Ing. Ondřej Žižlavský, PhD, Eddie Fisher, and Tetyana Shpilka (BUT)
Red Hat investigators: Marcel Gazdík, Vojtěch Sokol, and Tomáš Meszároš
The practical application of our Innovation Scorecard concept in three case studies within Red Hat has now been successfully completed.
The primary focus of the first two case studies was limited to agile software development. This focus was ideal for our team to check how valid and reliable the developed concept of measuring the success of any change or innovation had been. The first case study, known as Atomic Host (container automation), allowed us to review the initial theoretical concept and get it into better shape for the case studies that followed. The second case study, known as CI, was more challenging due to the technical complexities associated with continuous integration. This opportunity drove the need to adjust the initial concept so it could be better applied for this project. It worked well and we updated our stage/gate process accordingly.
The third case was fundamentally different and brought with it some demanding challenges in technical, communication, and people management areas. This case study is known as Global Wi-Fi Rollout (still ongoing). It was our chance to test the Innovation Scorecard in a non-agile software development area.
Based on the positive feedback received from the Red Hat teams involved in this initiative, we can report that the Innovation Scorecard has been well received and has made significant contributions toward identifying and improving work processes including communications, empowering people, and reducing error/bug rates.
We successfully completed the following activities:
- Development, design, and verification of an Innovation Scorecard Methodology (certified by the Czech Society for Quality)
- Publication of our Innovation Scorecard Methodology by Springer Verlag (Germany) at the end of 2021
- Series of related research articles published by the Project Management Institute (PMI) during 2021
- Innovation Scorecard Presentation in September 2021 (organized by Red Hat)who wish to apply the Innovation Scorecard in their work area
- Made associated templates and worksheets freely available on our website (iscorecard.org) to provide help and support to those who wish to apply the Innovation Scorecard in their work area
The Vega Project rack, nicknamed “REK”
PROJECT: Vega Project
Academic investigators: Gabriel Szász (Masaryk)
Red Hat investigators: Nikolaos Moraitis, Zdeněk Švécar, and Filip Hubík
Our research group has already collected some intriguing evidence that rotation has a significant impact on the parameters and evolution of stars. We just need to prove these findings on a larger scale to convince a broad scientific community. In order to build the new model atmosphere grid for the rotating main-sequence stars, which will help prove our case, we needed more computing power.
The project is using Red Hat® 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. Through a Red Hat Research donation to Masaryk University—Faculty of Science, we received sixteen servers. We delivered supporting IT infrastructure (e.g., rack, PDUs, etc.), and the stack is now built in the Masaryk University datacenter. At the moment, we are in the process of streamlining the OpenShift installation onto sixteen bare metal nodes. This will be our basis for the actual modeling of stellar atmospheres.