eature models are a commonly used technique for modeling software variability and representing possible configurations of a system. This paper presents the llhsc tool, which is designed to generate and check device trees for custom hardware based on the constraints specified in a feature model. The form
of these constraints is a set of logical formulas, which enables product line validation using off-the-shelf satisfiability solvers. For checking purposes, a new set of constraints is defined, which includes the specification of both syntax and semantic correctness of a delta-oriented software product line for DeviceTree bindings. This approach provides a more general and flexible solution for configuring static-partitioning hypervisors, but can also be used in systems without virtualization support, enabling the tool to be used in various contexts without sacrificing its generality. Through an empirical running example, we demonstrate the effectiveness of our approach, providing evidence that supports the construction of customized configurations for systems running static-partitioning hypervisors.
Abstract
This work is supported by the European Union/Next Generation EU, through Programa de Recuperação e Resiliência (PRR) [Project Route 25 with Nr. C645463824-00000063].
Conclusion
The approach we have presented offers a constructive way to safely configure embedded systems through the use of a feature model and a series of deltas applied to a master DTS. The llhsc tool ensures the correctness of the DOP product line through a set of constraints defining the syntactic and semantic aspects that can be proven correct by the Z3 SMT solver. The generation of proof obligations for syntactic correctness is done by composing the schemas of individual DT bindings, while semantic validation of memory addresses and interrupts is performed using bit-vector constraints. The extensibility of the llhsc tool allows for the incremental addition of constraints to the same Z3 instance, making it a versatile tool for future work. Overall, the effectiveness of this approach has been demonstrated in the configuration of a hypervisor, providing a safe and efficient method for resource allocation.
Relevant Resources
Access complete Publication
For an in-depth exploration of our findings and methodologies, download here
