Main Content

Analyze Formal Requirements of an Electric Vehicle Charger Locking Mechanism

This example uses a Requirements Table block to define a set of formal requirements used by a model of an electric vehicle charger locking system. After creating formal requirements for the locking system, you analyze the requirements for issues that can prevent the requirements from being complete and consistent. Once you identify the issues, you adjust the requirements.

When charging an electric vehicle, the charging port of the vehicle can be exposed to high voltages, which can be dangerous to consumers without proper safeguards. Electric chargers and vehicles deploy locking mechanisms to prevent customers from being exposed to these voltages. To ensure the locking mechanism activates and deactivates without creating hazards, the charging station provides signals to the vehicle before, during, and after charging. The vehicle uses those signals to determine when the charging cord can be unlocked and is safe to handle.

View the Formal Requirements

Open the model, CordLockReqTable_v1.


This model adapts the signals used by the charging station from the standard SAE J1772 [1]. To capture the signals, the Requirements Table block uses six input ports that are associated with input data of the same name. See Define Data in Requirements Table Blocks.

The input data are:

  • ChargeStatus: The charging status of the vehicle. The status indicates that the vehicle is not charging (NotCharging), charging (ChargeStart), shutting down (NrmlShutDown), or performing an emergency shut down (EmrgShutDown).

  • EvseType: If the vehicle is compatible with the charging station or not. The vehicle can be Compatible, Incompatible, or undecided (NotDecided).

  • PilotStatus: The pilot status of the charging station. The pilot status indicates if the charging station is on standby (A), if the charging station detects the vehicle (B), if the charging station detects the vehicle and that the vehicle is ready to charge (C), if the charging station detects the vehicle and that the vehicle is ready for charging in a ventilated area (D), or if there is an error (E_F). States B, C, and D each have two substates. Substate 1 indicates that the charging station is not ready to charge, and substate 2 indicates that the charging station is ready to charge.

  • SessionStopResMsg: Whether the termination of the charging session has been acknowledged by the charging station (Received) or not (NotReceived).

  • Vinlet: The voltage of the charging port measured by the vehicle.

  • LockCommand: The status of the lock. The lock can either be Locked or Unlocked.

The block uses the value of the input data to set the Type property of the data to an enumerated value specified in a MATLAB® program file. For example, the ChrgStat.m file contains the available statuses for the ChargeStatus data.

Open the block to view the requirements. The Requirements tab lists three simple requirements:

  1. The electric vehicle shall lock the cord in place if the electric vehicle supply equipment is compatible.

  2. The electric vehicle shall unlock the cord if the acknowledge terminate charging session signal is received and the vehicle measures an input voltage that is less than 60 V during normal shutdown procedures.

  3. The electric vehicle shall unlock the cord if the pilot status is not ready and the vehicle measures an input voltage that is less than 60 V during an emergency shutdown.

Each requirement specifies the checked conditions the Precondition column. If the requirement precondition is satisfied, the block then verifies that the appropriate locking status occurs in the postconditions, specified in the Postcondition column. For example, in the first requirement, the specified precondition checks if the vehicle type is compatible. If true, the block checks if the cord is locked, specified in the postcondition.

Analyze the Requirements for Issues

After creating a requirement set in the block, confirm that the requirements uniquely define the data captured, stored, and generated by the block. In this example, you use Simulink® Design Verifier™ to detect issues in your requirement set for you. These issues are adapted from the ISO/IEC/IEEE 29148 standard [2]. In this example, Simulink Design Verifier detects two kinds of issues:

  1. Inconsistency Issues: The block detects a scenario where the data can equal more than one value during simulation.

  2. Incompleteness Issues: The block detects a scenario where the data is not defined during simulation.

To analyze the table, in the Table tab, in the Analyze section, click Analyze Table.

Update the Requirements

To resolve the issues, you need to update the requirements. For example, to alleviate the inconsistency issue, update the precondition in the first requirement so that the charge status must be charging and the charger must be compatible with the vehicle.

After updating the precondition, run the analysis again to confirm that you have fixed the inconsistency issue.

This update does not resolve the incompleteness issues. To do that, the requirements must specify values for the data defined in the block throughout the simulation. Iterate through updating and analyzing the requirements to resolve these remaining issues.

Open the model CordLockReqTable_v2 and open the Requirements Table block to see an example of a complete requirement set.


The table includes additional input data, ChargePlug, that specifies if the cord is plugged into the vehicle (Plugged) or not (NotPlugged). The requirement set also includes five additional requirements. To improve readability, the requirements have been rewritten to use additional column headers.

When you design requirements, you must consider the physical limitations of your system. For example, if you develop a requirement that specifies a diameter, you must ensure the diameter cannot be negative. To account for the physical limitations of the system, specify assumptions in the Assumptions tab. See Add Assumptions to Requirements. In this example, the Requirements Table block includes three assumptions.

  1. If the pilot status is on standby (A), then the car is not charging.

  2. If the vehicle is not compatible with the charger, then the vehicle is not charging.

  3. If the charger is not plugged in, then the vehicle is not charging.

To view the assumptions, click the Assumptions tab.

If you run the analysis on this requirement set, Simulink Design Verifier does not detect issues.


[1] Hybrid - EV Committee, “SAE Electric Vehicle and Plug in Hybrid Electric Vehicle Conductive Charge Coupler” (SAE International), accessed December 21, 2021,

[2] “29148-2018 - ISO/IEC/IEEE International Standard - Systems and Software Engineering -- Life Cycle Processes -- Requirements Engineering” (IEEE), accessed December 21, 2021,

See Also

Related Topics