The way forward: Unlocking by verification

For thermometers, sewing machines and cars the embedded software revolution gained momentum at a time too early to realise the lock-in problem. For bicycles there is a good chance to do things different, because (i) the consequences are now apparent, (ii) a considerable share of bicycles is self-maintained, and (iii) there is a tradition of modularity and interoperability of components which often are inexpensive.

But bicycles are safety-critical: fiddling with an e-suspension software does not seem a good idea, unless the fiddler is supported by tools helping to understand the physics implications and software limitations. The POWVER project shall explore precisely that. It will develop modern computer-assisted verification technology to provide a basis for unlocking the electric mobility of the future, set up as a blueprint for other battery-powered appliances. As such, POWVER is the starting point for a radical change in the way embedded software quality is assured in general.

At the technical core of POWVER is quantitative verification. This is a branch of computer science research that bridges deep foundational investigations with tool-oriented and applied development of embedded systems. It enables formal and automated reasoning about aspects of embedded software related to time, continuous dynamics, probabilities, or costs. It has seen rapid advances in academia and research over the past decades.

Read on to learn about POWVER Quantitative Verification.