Database of Case Studies Achieved Using CADP

Modeling, Verification, and Test-case Generation for the EnergyBus Standard

Organisation: Saarland University, Germany

Method: LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)
TGV (Test Generation with Verification technology)

Domain: Embedded Systems

Period: 2013-2014

Size: 1700 lines of LNT code (+200 lines of comments)

Description: 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 EnergyBus-compliant.

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.

Conclusions: 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:
  • 1. missing counter value data in SYNC message reception;
  • 2. missing state change in the LSS FSA during configuration process by slave devices;
  • 3. wrong behaviour of unconfigured slaves in the LSS Fastscan protocol
There is a clear return on the investment in developing formal specifications. Our work shows that model-based testing approaches are applicable, if not directly out of the box, at least without too much stretching, i.e., using simple abstraction techniques. The LNT language, which had not been used priorly for field bus protocols, has shown to be a beginner-friendly notation and provided a formal basis for discussing with the EnergyBus experts. Furthermore, the CADP tools (especially the LNT translator) benefited from the EnergyBus modelling feedback.

Publications: [GrafBrill-Hermanns-Garavel-14] 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

Contact:
Holger Hermanns
Saarland University
Computer Science
66123 Saarbrücken, Germany
E-mail: hermanns@cs.uni-saarland.de
Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page