Study of the COQ Proof Assistant, application to Real-time scheduling

Advisor Joël Goossens
Keywords RTOS, scheduling, Automatic proof

Description

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. Citation https://coq.inria.fr/

The student will study the COQ tool and language. Then the student will illustrate how to use that tool in the framework real-time scheduling properties using example based upon real-time literature.

References

  • Coq@Inria
  • Cerqueira, Felipe, Felix Stutz, and Björn B. Brandenburg. “PROSA: A Case for Readable Mechanized Schedulability Analysis” 28th Euromicro Conference on Real-Time Systems (ECRTS), 2016. PDF

Compatibility with the Device Tree standard

Advisor Joël Goossens
Keywords RTOS, device driver

Description

The device tree standard devicetree.org is a way to describe the hardware target an operating system is running on. It describes the memory layout (address of the different I/O peripherals and devices, memory banks), different features such as the number of cores, the frequency of the clocks… This information is written in so-called device tree files that follow a specific format. Device trees are widely used for Linux. Due to historic reasons HIPPEROS developed its own (simpler) device tree in the form of Python code. This means that for every architecture developers must redefine the information they deem useful in our custom format. This is error-prone and time consuming. We wish to use the standard device tree format instead in order to reuse the existing base of device tree files. For technical reasons, we cannot simply reuse the device tree parsing tools that have been developed for other operating systems.

The intern will:

  • develop/improve a custom device tree parser that will generate the information in a format usable by the HIPPEROS RTOS;
  • Replace the existing device tree by the newly developed one and simplify the code that relies on it in the kernel and device drivers.

Image Processing Demo on a hybrid CPU-FPGA target

Advisor Joël Goossens
Keywords RTOS, FPGA, computer vision

Description

As part of the TULIPP project tulipp.eu HIPPEROS wishes to demonstrate a hybrid image processing application that takes advantage of a modern heterogeneous FPGA/CPU platform, the Xilinx Zynq 7000 System on Chip (SoC). This SoC integrates a dual-core ARM CPU and a FPGA. The application will perform the heavy duty rendering on the FPGA and additional background tasks on the CPU.

The intern will:

  • develop the demo application based on the image processing filters currently used at HIPPEROS for the FPGA part and the HIPPEROS RTOS for the CPU part;
  • develop new filters to develop a more sophisticated demonstrator;
  • develop stress tests and benchmarks in order to show the processing power leveraged by the FPGA side and the flexibility of the CPU.

Implement driver to support L2 cache in the HIPPEROS kernel

Advisor Joël Goossens
Co-Advisor Juan M Rivas (ULB/Hipperos)
Keywords RTOS, cache, driver, kernel

Description

Modern processors implement cache memory which is designed to close the gap between the ever-increasing speed of the processors and the lagging system main memory. Intelligent use of the cache can greatly improve the average case execution time of applications, and it is usually a target of compiler based optimisations. On the other hand, cache memory can also add high levels of unpredictability in the execution times of the applications, which makes the usage of cache problematic in real-time embedded systems, in which the worst-case behaviour is the most important.

A new topic of interest in both the industry and the academia involves re-enabling the cache in real-time systems, and using it in new ways that can in fact improve the predictability of multi-core processors. As a first step towards this goal, we wish to add support, inside the HIPPEROS kernel, for the L2 cache, which is typically the larger cache that is shared between the cores.

Real-time obstacle detection for Unmanned Aerial Vehicles

Advisor François Quitin (ULB, Beams)
Co-Advisor Joël Goossens
Keywords RTOS, 3D, UAV

Description

Proposal of common internship and master thesis with ULB BEAMS (Prof. François Quitin).

In a previous internship a 3D mapping application using a lidar and a drone using the HIPPEROS RTOS was developed. The application is used to demonstrate the use of the RTOS on a real-life system. We wish to extend the features of the demo application by developing an obstacle avoidance system using the lidar. The intern will use the information collected from the lidar in real-time and implement an obstacle avoidance system. More information on beams.ulb.ac.be.

Porting of the OpenCV camera vision library

Advisor Joël Goossens
Keywords RTOS, Computer Vision, OpenCV

Description

OpenCV (Open Source Computer Vision Library) is an open source computer vision and machine learning software library. OpenCV was built to provide a common infrastructure for computer vision applications and to accelerate the use of machine perception in the commercial products. Being a BSD-licensed product, OpenCV makes it easy for businesses to utilize and modify the code.

HIPPEROS is currently taking part to the TULIPP project tulipp.eu. One of the goals of the project is to simplify the development of image processing and camera vision applications on the HIPPEROS RTOS using the OpenCV library.

The intern will work in cooperation with the development team and will:

  • port the library on HIPPEROS;
  • develop a demonstration application on a reference platform;
  • analyze dependencies between the library and the underlying operating system.

Porting of HIPPEROS on the Xilinx Zynq UltraScale+ platform

Advisor Joël Goossens
Keywords RTOS, Zynq-7000 UltraScale+

Description

The goal of the internship (and the master thesis) is to integrate the Zynq-7000 UltraScale+ platform as a new target device for the real-time operating system HIPPEROS.

This platform will be used for medical and transportation use cases within the framework of real-time image processing applications. The intern will have the responsibility to add support for this board and run HIPPEROS applications on it. The intern will then develop the Board Support Package and the drivers of the peripherals of the platform and the board (timers, interrupt controller, power management unit, boot- loader, etc.) The intern will be supervised by a senior software engineer of the HIPPEROS kernel development team that will help him to realize his tasks and to learn the necessary skills. The intern will be integrated as a member of the development team and will practice the methodologies and processes of the company (Scrum methodology, decentralized code review, etc.). The intern will have to communicate with the members of the development team to facilitate his/her work and will have to periodically communicate to the team and management about his/her technical progress. HIPPEROS will provide to the intern all the necessary material to accomplish his/her work (desktop computer, embedded development board, documentation). Reference: xilinx.com