Saarland University, Germany
CADP (Construction and Analysis of Distributed Processes)
TGV (Test Generation with Verification technology)
1700 lines of LNT code (+200 lines of comments)
The EnergyBus is an upcoming industrial standard, based on the
CANopen field bus for electric power transmission and management.
This standard aims at ensuring interoperability between chargers
and batteries of Light Electric Vehicles, and, more generally,
to ensure interoperability between all electric components so
that one eventually can freely combine battery pack, motor,
charger, and even the dashboard, as long as all devices are
At the core of EnergyBus is a universal plug integrating a CAN-Bus with switchable power lines. Beyond standardised plugs and sockets, one also needs a protocol stack that orchestrates the exchange of messages and guarantees safe interoperation.
The LNT language was used to formally describe the EnergyBus protocol (1700 lines of LNT code). This formal description in LNT was processed using the LOTOS and LNT compilers and verification tools of the CADP toolbox.
Based on the TGV model-based test generator, a tool platform was developed for the automatised conformance testing of EnergyBus implementations against the formal description in LNT. This platform can also be used for testing CANopen devices as well, since the LNT description also models CANopen aspects.
The formal specification work and the computer analysis of the
LNT specifications revealed various ambiguities and inconsistencies
in the EnergyBus description.
The platform allowed to detect three deviations in the CANopen
software stack used for the experiments:
Alexander Graf-Brill, Holger Hermanns, and Hubert Garavel
"A Model-Based Certification Framework for the EnergyBus Standard".
Proceedings of the 34th IFIP WG 6.1 International Conference on
Formal Techniques for Distributed Objects, Components, and Systems
(FORTE 2014), June 2014, Berlin, Germany
Available on-line at: http://cadp.inria.fr/publications/GrafBrill-Hermanns-Garavel-14.html
66123 Saarbrücken, Germany
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|