Back to the study

Glossary

The specialist terms used on this site, in plain English. On the study page, each dotted term opens the same explanation.

EVerest and OCPP

EVerest: Open-source software for running an electric-vehicle charging station, maintained as a Linux Foundation Energy project. This study tested its code for combining charging schedules.; Pionix GmbH started EVerest, and it is released under the Apache 2.0 licence. It supports OCPP 1.6 and 2.x.; The study tested its unchanged C++ code that works out a charger’s power limit from its schedules, at source revision dd696165. EVerest documentation (opens in a new tab)
OCPP: Open Charge Point Protocol: shared rules for communication between electric-vehicle charging stations and the software managing them. This study checks charging schedules under version 1.6.; The Open Charge Alliance publishes it. Version 1.6 came out in 2015 and is widely used.; In version 1.6, the network can send a charger schedules that cap how much power it gives. OCPP calls a schedule a charging profile, so the site sometimes says “profile” too.; Each schedule is a list of periods. Each period starts at an offset from the schedule’s start and has a limit in amps or watts. Daily and weekly schedules repeat.; A charger can hold charger-wide, default and transaction schedules at once. It combines them into one limit for each moment. OCPP 1.6 edition 2 (zip) (opens in a new tab)
Schedule anchor: The moment a schedule first started. A daily schedule restarts at that time of day. The study groups its test cases by the year of the anchor.; In the study’s smallest example, the schedule’s anchor is 11:00:00 UTC on 14 September 2016.; When anchors fall in 2017–2025, all 2,000 generated cases pass. When they fall in 2010–2016, 835 pass, 92 get a warning and 1,073 fail. A warning marks a difference the rules allow but the study flags, such as a limit below the reference model’s, which loses charging.; The study traces the failures to the leap seconds since the anchor.
Leap second: An extra second sometimes added to clock time to keep it in line with Earth’s rotation.

Proof

Reference model: A program describing the behavior we expect. We compare its answers with the code being checked. It covers only the behavior it describes.; The study’s reference model is written in Lean, so the site also calls it the Lean model, or the model for short.
Lean: A language for precisely describing how code should behave, and a tool for checking mathematical arguments about those descriptions.
Proof: A computer-checked mathematical argument that a rule always holds under stated assumptions. It does not tell us whether the rule is the right one.

Tests

Differential testing: Run the same chosen inputs through two programs and compare their answers. A difference needs investigation. Matching answers cover only the inputs tried.
Tolerance: How close two limits must be to count as agreeing: within 0.05 of the profile’s unit, amps (A) or watts (W).
Vacuous pass: A passing case where the reference model gives no limit at any instant compared, so there was nothing to agree with.; The study’s report counts 55 such cases when anchors fall in 2017–2025, and 64 when they fall in 2010–2016.

Assumptions

Trusted base: The parts assumed to work correctly for a result to hold, such as the program checking the proof and the program running the tests.

People

Signed reading: The interpretation of the standard that Harry approved in the signed spec. Where the standard’s wording allows more than one reading, the study follows this one.; The finding holds under this reading.; The standard’s wording allows another reading too. Once a leap second falls between a schedule’s start and now, “every 24 hours” could mean 24 hours of elapsed seconds, which is what EVerest counts.; Harry’s decisions are labelled A1 to A10 in the signed spec.
Correspondence review: An AI review that searched for mismatches between the model and the written rules. Its findings needed Harry’s decision and do not count as evidence.