Florian Jost, Carsten Sinz
Technical Track
 | Haus der Universität, Schlösslistrasse 5, 3008 Bern, Switzerland |
 | 8 February 2024, 11:20 CET |
 | Florian Jost |
 | Pierre Martou |
 | https://dl.acm.org/doi/10.1145/3634713.3634728 |
Car manufacturers offer their customers an enormous number of configuration options. In the process, the variance is also increasing in the provided software. For exclusion of incompatible configurations, complex control systems are created using propositional logic. To check the feasibility of an order, all these constructability conditions must be satisfied. This check is called a “constructability check” and is carried out with the help of SAT solvers. Originally intended only for checking hardware configurations, the existing systems have been extended to also include software components. For software dependencies, however, Satisfiability Modulo Theory (SMT) solvers seem more appropriate in modern versioning approaches as they can also handle numerical domains. We propose a model in Quantifier-Free Integer Difference Logic (QF-IDL) to describe hardware/software configurations in the automotive context. Using our model, we demonstrate how to solve software installation and software update problems.