Repository navigation
Xin Zhao Notebook
Co-simulation
Substation
Formal Verification
8/24 - 8/27
- Based on the initial presentation from the first week, I conducted preliminary research on various topics, including substation components, ROS development, and the Cyber-Physical System.
8/28 - 9/3
- Watched some HELICS tutorial videos from: https://www.youtube.com/@tdc-helics9643
9/4 - 9/10
- Following the provided instructions, I have completed the initial setup of the environment on my Ubuntu guest system.
9/11 - 9/17
- Conducted preliminary research on substation hierarchy and IEC 61850.
- When I first ran the provided
run_example.shscript, an error message appeared, indicating "No such file or directory." In response to this initial error, I proceeded to modify therun_example.shshell script:
#!/bin/bash
# Set the root directory of your repository
REPO_ROOT="/home/xzhao/Desktop/cps/cps-cosimulation-env"
mkdir -p "$REPO_ROOT/results"
TIMESTAMP=$(date +%s)
BROKER_LOG="$REPO_ROOT/results/broker_$TIMESTAMP.log"
TRANSMISSION_LOG="$REPO_ROOT/results/TransmissionSim_$TIMESTAMP.log"
DISTRIBUTION_LOG="$REPO_ROOT/results/DistributionSim_$TIMESTAMP.log"
touch "$BROKER_LOG"
touch "$TRANSMISSION_LOG"
touch "$DISTRIBUTION_LOG"
# Start the HELICS broker in the background
"$REPO_ROOT/install/bin/helics_broker" -t="zmq" --federates=3 --name=mainbroker > "$BROKER_LOG" 2>&1 &
# Start Transmission simulation
cd "$REPO_ROOT/simple_gridlabd_example/Transmission"
python3 Transmission_simulator.py > "$TRANSMISSION_LOG" 2>&1 &
cd "$REPO_ROOT"
# Start Distribution simulation with gridlabd
cd "$REPO_ROOT/simple_gridlabd_example/Distribution"
gridlabd IEEE_123_feeder_0.glm > "$DISTRIBUTION_LOG" 2>&1 &
cd "$REPO_ROOT"
# Start Relay simulation
cd "$REPO_ROOT/simple_gridlabd_example/Relay"
exec python3 Relay_simulator.py
cd "$REPO_ROOT"
When I execute the modified run_example.sh script once again, I am able to successfully execute the example:

9/18 - 9/24
- Compiled the Research Documentation (https://shorturl.at/alQRY), which consists of some research questions related to
Co-simulation,Substation,IEC 61850,Project Architecture,Directory Hierarchy, andDesign Proposals.
9/25 - 10/1
-
Drafted the project directory structure for a three-level substation, without considering the Object-Oriented Programming (OOP) paradigm.
-
Concluded the general process to implement co-simulation in HELICS:
- Define Federates:
- Identify substation devices (e.g., Protection Relays, Bay Controllers).
- Create Python programs for each with JSON configurations.
- Configure Communication:
- Determine data exchange needs (values) between devices.
- Specify publications (pubs) and subscriptions (subs) in federate JSONs.
- Create HELICS Runner JSON:
- Develop a runner file (e.g.,
helics-config.json) to specify:- HELICS broker setup.
- Federate launch commands.
- Develop a runner file (e.g.,
- Launch the Co-Simulation:
- Run the co-simulation using the HELICS runner.
- Monitor and Analyze:
- Observe device interactions and collect data.
- Analyze results for research insights.
- Refine as Needed:
- Adjust models or co-simulation setup based on findings.
- Define Federates:
-
Drafted typical networked devices in a substation in Python:
class NetworkedDevice:
def __init__(self, device_name, device_type, communication_protocol):
self.device_name = device_name
self.device_type = device_type
self.communication_protocol = communication_protocol
self.status = "Inactive" # Default status
def activate(self):
self.status = "Active"
def deactivate(self):
self.status = "Inactive"
def get_status(self):
return self.status
def get_device_name(self):
return self.device_name
def get_device_type(self):
return self.device_type
def get_communication_protocol(self):
return self.communication_protocol10/2 - 10/8
- Revised the code to implement a three-level substation hierarchy in Python using OOP:
class Device:
def __init__(self, name: str, communication_protocol: str):
self.name = name
self.communication_protocol = communication_protocol
self.status = "Inactive" # Default status
def activate(self):
self.status = "Active"
def deactivate(self):
self.status = "Inactive"
def get_status(self) -> str:
return self.status
def get_device_name(self) -> str:
return self.name
def get_communication_protocol(self) -> str:
return self.communication_protocol
# Process Level Device:
class ProcessLevelDevice(Device):
def __init__(self, name, communication_protocol):
super().__init__(name, communication_protocol)
class Sensor(ProcessLevelDevice):
def __init__(self, name, communication_protocol, parameter_measured):
super().__init__(name, communication_protocol)
self.parameter_measured = parameter_measured
def measure(self):
# Implement code to measure the parameter and return the value
pass
# Bay Level Device:
class BayLevelDevice(Device):
def __init__(self, name, communication_protocol):
super().__init__(name, communication_protocol)
class Relay(BayLevelDevice):
def __init__(self, name, communication_protocol, protection_function):
super().__init__(name, communication_protocol)
self.protection_function = protection_function
def perform_protection(self):
# Implement code to perform the protection function
pass
class BayController(BayLevelDevice):
def __init__(self, name, communication_protocol, bay_number):
super().__init__(name, communication_protocol)
self.bay_number = bay_number
def control_equipment(self, equipment):
# Implement code to control equipment in the bay
pass
# Station Level Device:
class StationLevelDevice(Device):
def __init__(self, name, communication_protocol):
super().__init__(name, communication_protocol)
class StationGateway(StationLevelDevice):
def collect_data(self, devices):
# Implement code to collect data from multiple devices
pass
class HumanMachineInterface(StationLevelDevice):
def display_data(self, data):
# Implement code to display data on the interface
passConduct some research on how to apply formal verification to the Sensor class:
- Specification: Define expected behavior, properties, and safety criteria.
- Formal Model: Create a mathematically precise model.
- Verification Tools: Use formal tools to check if the model meets specifications.
- Testing: Perform comprehensive testing for various scenarios.
- Security: Ensure secure communication and address vulnerabilities.
- Concurrency: Verify proper handling of concurrency.
- Safety: Comply with safety standards if necessary.
- Documentation: Maintain clear records of specifications and results.
- Tools: TLA+, Z3, SPIN
- On Thursday, our group presented the IPR 1 Presentation. We aim, from the perspective of the Pacific Northwest National Laboratory, to address critical challenges at the intersection of smart grids and national security. How can we integrate cyber-physical security into the smart grid to enhance resilience while ensuring efficient collaboration among various components and safeguarding against defects in the smart grid ecosystem? Therefore, the upcoming phase of my development and research will be more focused on MITRE ATT&CK ICS and formal verification.
- Reconstructed the Gantt chart using the Jira platform, incorporating a detailed schedule organized by teams.
- Formulated several potential scenarios based on our ongoing research, and I'll be discussing their feasibility with Samuel for confirmation:
-
Devices:
Circuit Breaker,Transformer,Bay Controller,Protection Relay -
Scenarios:
-
Fault Detection and Clearing:
- Simulate a fault in the power system, such as a short circuit or overcurrent event.
- The protection relay detects the fault and sends a protection trip signal to the circuit breaker via the IEC 61850 network.
- The circuit breaker opens to isolate the faulted section of the network.
- The bay controller supervises the operation, collects data, and sends status updates.
-
Transformer Overloading:
- Simulate increased load demand or a transformer malfunction.
- Monitor the transformer's loading conditions and temperature.
- When the transformer approaches overload conditions, the bay controller can send a signal to a load-shedding scheme to reduce the load.
-
Voltage Regulation:
- Introduce variations in the voltage levels within the grid.
- The bay controller monitors the voltage levels at the substation and adjusts the transformer tap settings to maintain voltage within acceptable limits.
-
Fault Detection and Clearing:
-
Devices:
- Structured the research paper in Overleaf and assigned tasks.
10/9 - 10/15
- Researched and archived academic papers for our project in my personal repository
10/16 - 10/22
- Completed the initial
CircuitBreakerdraft and designed unit tests, with a success rate of 6 out of 7. Currently addressing an issue withtest_default_state, to be resolved later. - Completed the midterm research paper
10/23 - 10/29
- Created a detailed Project Task Breakdown for the remainder of the semester:
Project Task Breakdown
Scenario: Voltage Regulation
Objective: Introduce variations in voltage levels within the grid to assess the grid's performance.
-
Task 1: Voltage Monitoring and Control
- Develop a bay controller to monitor voltage levels at the substation.
- Implement a control mechanism to adjust transformer tap settings to maintain voltage within acceptable limits.
-
Task 2: Fault Injection
- Utilize fault injection to assess the system's response to simulated faults.
Co-simulation Subteam
-
Task 1: Set up the co-simulation environment and run the
simple_gridlabd_example(Completed) -
Task 2: Core Code and API Documentation
- Analyze the simple_gridlabd_example and Electric Vehicle example from HELICS to identify core code components and APIs.
- Document findings in the Research Documentation.
-
Task 3: Co-simulation Scenario Design
- Define the specific scenarios for voltage variations within the grid.
- Determine the timing and parameters for voltage level changes.
- Write the framework code for the specific scenario.
-
Task 4: Real-time Data Monitoring
- Implement a real-time monitoring system to track voltage levels during co-simulation.
- Enable visualization and data recording for analysis within the co-simulation environment.
-
Task 5: Fault Tolerance and Recovery
- Implement mechanisms for fault tolerance and recovery to ensure simulation integrity.
Device Modeling Subteam
Device modeling must adhere to a fail-hard contract-based approach, ensuring that errors are immediately reported when encountered, rather than attempting to gracefully handle them. This aligns with the Design by Contract (DbC) principles, simplifying debugging and enforcing the integrity of contract conditions.
-
Task 1: Set up the co-simulation environment and run the
simple_gridlabd_example(Completed) -
Task 2: Circuit Breaker
- Develop a model for the circuit breaker that can open and close to protect the grid from faults.
- Ensure the model responds to signals from protection relays.
-
Task 3: Transformer
- Create a model for the transformer that accurately reflects its behavior in response to changing tap settings.
- Implement the ability to adjust tap settings based on commands from the bay controller.
- Task 4: Bay Controller - Integrate the bay controller with the models for circuit breakers and transformers.
-
Task 5: Protection Relay
- Develop a model for protection relays to detect and respond to faults within the grid.
-
Task 6: Voltage Monitoring and Reporting
- Implement voltage monitoring functionality for devices like transformers and circuit breakers.
- Create a reporting mechanism to transmit voltage data to the bay controller.
-
Task 7: Integration Testing
- Collaborate with the Co-simulation Subteam to validate device models within the co-simulation environment.
- Verify that the models respond appropriately to voltage variations.
Network Protocol Integration Subteam
-
Task 1: Set up the co-simulation environment and run the
simple_gridlabd_example(Completed) -
Task 2: Communication Protocol Design
- Research specific scenarios and define communication protocols for data exchange between devices, the bay controller, and protection relays.
- Select suitable communication standards and design message formats.
-
Task 3: Protocol Implementation
- Develop code to implement the chosen communication protocols.
- Ensure that devices can transmit and receive data using these protocols.
-
Task 4: Simulation Data Exchange
- Enable data exchange between GridLAB-D and HELICS through the established communication protocols.
- Test and verify the reliability of data transmission.
Start by connecting to the GT VPN. Then, use the server domain ece-linlabsrv01.ece.gatech.edu and run ssh -XC <gatech-username>@ece-linlabsrv01.ece.gatech.edu -p 22 to access the server. Unfortunately, it appears I lack the necessary permissions to install the required utilities.
[xzhao455@ece-linlabsrv01 /]$ ls
bin boot dev etc home lib lib64 media mnt nethome opt proc root run sbin srv sys tmp tools usr var
[xzhao455@ece-linlabsrv01 /]$ sudo visudo
[sudo] password for xzhao455:
xzhao455 is not in the sudoers file. This incident will be reported.
[xzhao455@ece-linlabsrv01 /]$ su -
Password:
su: Authentication failure
[xzhao455@ece-linlabsrv01 /]$ lsb_release -a
LSB Version: :core-4.1-amd64:core-4.1-noarch:cxx-4.1-amd64:cxx-4.1-noarch:desktop-4.1-amd64:desktop-4.1-noarch:languages-4.1-amd64:languages-4.1-noarch:printing-4.1-amd64:printing-4.1-noarch
Distributor ID: RedHatEnterprise
Description: Red Hat Enterprise Linux release 8.8 (Ootpa)
Release: 8.8
Codename: Ootpa
[xzhao455@ece-linlabsrv01 /]$
The CircuitBreaker unit tests passed.
10/30 - 11/5
- Addressed
Bay Controllerissues, passed basic unit tests, enabled voltage adjustment with margin voltage, and added value visualization:
- Also, made
Transformermodifications for consistent variable names and data type annotations.
11/6 - 11/12
Made the voltage regulation scenario more specific and refined:
- Scenario Description: During the nighttime, the electrical power system may face challenges related to voltage fluctuations, especially during peak periods or unexpected load variations. This simulation scenario aims to assess the voltage regulation performance of a substation to ensure that the voltage remains within acceptable limits.
-
Communication Protocols:
- Modbus is used for communication between the bay controller and the main transformer to adjust tap settings and monitor voltage.
- DNP3 is used for communication between devices to transmit fault information for coordinated response, ensuring system reliability and response speed enhancement.
- Scenario Time: Nighttime, typically between 22:00 and 04:00.
- Execution Steps:
-
Initial State: The substation is in normal operational mode, and the power network is at the standard voltage level.
Time: 22:00- Equipment:
Main TransformerBay ControllerCircuit BreakerSimulated Loads
-
Sudden Load Increase: Due to an unexpected event, the load suddenly increases, causing a voltage drop.
Time: 22:30
-
Voltage Monitoring and Control: The bay controller communicates with the main transformer using the Modbus protocol to monitor voltage levels. If the voltage falls below the set lower limit, the following steps are executed:
- Adjust the main transformer tap settings using Modbus commands to raise the voltage level.
- The bay controller records transformer settings and voltage data.
Time: 22:35
-
Substation Response: The main transformer responds to the setting changes, and the voltage gradually returns to the normal level.
Time: 23:00
-
Simulated Fault Injection: Simulated fault signals, such as short circuits or open circuits, are injected into the system using the DNP3 protocol to evaluate the system's response to faults.
Time: 00:00
-
Fault Response: Bay controllers and the main transformer communicate with other devices via the DNP3 protocol to transmit fault information. The power system begins to respond to faults, such as disconnecting affected lines or adjusting switch states.
Time: 01:00
-
Fault Recovery: The system successfully addresses the faults, and the voltage returns to the normal level.
Time: 02:30
-
End State: The simulation concludes, and the voltage returns to the standard level. Substation equipment continues to monitor and control voltage.
Time: 04:00
11/13 - 11/19
- Explored the Design by Contract tutorial, attempting to incorporate PyContracts and icontract into the built circuit breaker.
11/20 - 11/26
- Watched several videos on TLA+ and drafted a simple code example for an on/off switch:
-------------- MODULE DeviceModel --------------
EXTENDS Integers, Sequences, TLC
CONSTANTS MaxValue
VARIABLE state
Init ==
/\ state \in {0, 1} \* Assuming a binary state: 0 for off, 1 for on
On ==
/\ state = 0
/\ state' = 1
Off ==
/\ state = 1
/\ state' = 0
Toggle ==
\/ On
\/ Off
Next ==
\/ Toggle
Spec == Init /\ [][Next]_<<state>>
=============================================- state: Represents the state of the device (e.g., on or off).
- Init: Describes the initial state of the system. In this case, the device can be initially in either the on or off state.
-
On, Off, and Toggle: Operations that can be performed on the device.
Ontransitions the device from off to on,Offtransitions it from on to off, andTogglerepresents either turning it on or off based on its current state. - Next: Describes the possible next states of the system, specifying the allowed transitions.
- Spec: The overall specification, stating that the system should satisfy the initial conditions and should always be in a next state according to the specified transitions.
11/27 - 12/3
- Completed the finalization of our code repository and prepared for our final presentation.
12/4 - 12/8
- Structured the research paper in Overleaf and assigned tasks.
Co-simulation is an analysis technique that allows simulators from different domains to interact with each other, typically by exchanging values through the course of the simulation that define other simulators' boundary conditions. It breaks down the boundaries between individual simulators, allowing them to work together and calculate more realistic and dynamic results. Co-simulation is a method to model complex systems involving multiple interacting components or systems by coupling existing simulators. This approach can involve simulators representing various aspects of a system, such as atmospheric conditions, vegetation growth, ocean behavior, wildlife, and more. By enabling these simulators to communicate and share data, co-simulation creates a more comprehensive and accurate representation of the system's behavior. Key components of co-simulation include:
- Synchronization: Co-simulation requires maintaining synchronization among all simulator instances. This is essential when working in a heterogeneous simulation environment where simulators may have different concepts of time and varying computation times. Synchronization ensures that all simulators progress at a consistent pace, preventing some simulators from running too far ahead of others.
- Data Transfer: Co-simulation involves the exchange of data between simulators. Simulators must be able to send and receive data efficiently and accurately. This data exchange is crucial for simulators to influence each other's behavior and produce meaningful results.
- Integration: To enable co-simulation, simulators often need to be modified to support the framework (e.g., using a co-simulation middleware like HELICS). These modifications allow the framework to advance the simulator's time and provide new data values for specific variables.
When designing a co-simulation, the individuals responsible for integration must consider factors like the nature of the code base being integrated, the programming languages used, the simulator's concept of time, and the nature of the data exchanged between simulators. Co-simulation can be a powerful tool for modeling complex systems of systems, leveraging the strengths of existing simulators and improving the accuracy and realism of simulations.
In the context of co-simulation, it is important to understand the simulator's concept of time to effectively coordinate and synchronize processes:
- Time Step: Understanding the time step of each simulator is essential to ensure that the simulators are operating in a coordinated manner. Simulators may advance time in discrete intervals, and knowing the duration of these time steps helps in synchronization.
- User-Definable Time: Allowing users to define or modify time parameters, such as start time, end time, and time intervals, can be important for tailoring the co-simulation to specific requirements or scenarios.
- Time Concept: Knowing whether the simulator follows a continuous time concept or is event-based helps in understanding how actions and events are coordinated within the co-simulation environment.
Effective data transfer in co-simulation involves understanding the following key aspects:
- Inputs and Outputs: Identifying the primary inputs and outputs of each simulator is critical for ensuring that the necessary data is available for simulation and analysis. This information helps in setting up data flows and interactions between simulators.
- Boundary Conditions: Understanding the boundary conditions and assumptions made by each simulator about the external environment is essential for accurate and meaningful co-simulation results.
- Interdependencies: Recognizing the interdependencies between simulators is key to establishing the order and timing of data exchanges. Simulators often rely on data from other simulators to make decisions or calculations.
- Data Exchanges: Knowing what types of data will be exchanged between simulators, as well as adhering to specific data formats, protocols, or standards, is crucial for seamless communication and data sharing in a co-simulation environment.
The Hierarchical Engine for Large-scale Infrastructure Co-Simulation (HELICS) is a robust open-source framework designed for the co-simulation of cyber-physical-energy systems, particularly with a notable emphasis on integration with the electric power grid.
- Simulator: A simulator refers to the executable that performs specific analyses, typically generating a time series of values. It exists as software in a non-executing state outside of co-simulation. For example, you might hear phrases like, "This simulator does not accurately model xyz for this analysis" or "This simulator has been optimized for parallel execution on multi-core computers." When we discuss a specific instance of a simulator running a particular model, we are essentially referring to a real-time or virtual representation of the system or process under analysis, which generates data or results based on the defined mathematical, physical, or computational models and algorithms.
- Federate: Federates are the active instances of simulators assigned specific models and/or responsible for providing and receiving specific values from other federates. For instance, in a co-simulation involving ten distribution circuit models, all run by the GridLAB-D simulator, each of these becomes a unique federate contributing distinct values to others. A group of federates collaborating in a co-simulation is called a federation.
-
Model: A model is akin to an agent in the co-simulation. It encompasses the calculations within a simulator for a particular aspect of the simulation. Depending on the co-simulation requirements, a federate can be configured to host one or multiple models. For example, in an electric vehicle co-simulation, you might create a simulator to model the electric vehicle battery's physics and then configure the
Battery Federateto host multiple battery models and manage signal transfers to other federates. - Signals: Signals represent the information exchanged between federates during the co-simulation's execution. At its core, co-simulation relies on message-passing through these signals. HELICS classifies these messages into two categories: value signals and message signals. The former is used when connecting federates that share physical attributes (e.g., batteries supplying power to electric car wheel motors), while the latter is employed for connecting federates with informational interactions (e.g., battery charge controller and charge relay). The co-simulation offers various techniques and implementations for defining the nature of data exchange (such as data type) and data distribution throughout the federation.
- Interface: The interface is the structure that allows a federate to communicate with other federates. It comprises Endpoints, Publications, and Inputs.
- Core: The core is the software embedded within a simulator that enables it to participate in a HELICS federation. In most cases, each federate corresponds to a single core, effectively making the two terms synonymous (core ⇌ federate). The most common configurations include (1) one core, one federate, one model; (2) one core, one federate, multiple models. Occasionally, a single executable may represent multiple federates, with all of them utilizing a single core (one core, multiple federates, multiple models). Cores are designed around specific message buses, and HELICS supports various bus types. The selection of the message bus is part of the configuration process necessary for forming the federation.
- Broker: The broker is a specialized executable bundled with HELICS. It plays a crucial role in co-simulation by (1) maintaining synchronization within the federation and (2) facilitating message exchange. Each core (federate) must connect to a broker to be part of the federation. Brokers receive messages from connected federates and route them to their intended destinations. HELICS also supports a hierarchy of brokers, allowing federates associated with different brokers to communicate with each other, thus preserving the integrity of the federation. The highest-level broker in this hierarchy is called the root broker, which serves as the final message router.
HELICS leverages a number of underlying communication technologies to achieve the coordination between the co-simulation components. Some of these technologies are designed to be general in nature (such as ZeroMQ) and others are designed for particular situations (such as MPI in HPC contexts).
There are several different core/broker types available in HELICS, each providing advantages in particular circumstances depending on the architecture of the federation and the underlying computation and network environment on which it is executing. Generally speaking, the performance of the various cores is as follows (from best to worst):
- MPI
- IPC
- UDP
- TCP
- ZMQ: The ZMQ is the default core type and provides effective and robust communication for federations spread across multiple compute nodes. It uses the ZMQ mechanisms. Internally, it makes use of the REQ/REP mechanics for priority communications (such as queries) and PUSH/PULL for non-priority communication messages.
GridLAB-D is an innovative power system simulation tool, offering valuable insights to individuals involved in the design and operation of electric power transmission and distribution systems. Additionally, it serves as a valuable resource for utilities seeking to harness the benefits of cutting-edge smart grid technology.
A power system, also known as an electrical grid, is a complex network that delivers electrical energy from various sources to end-users efficiently and reliably. It consists of several key components and functions, including generators, substations, transmission lines, distribution lines, service transformers, and loads:
- Generators play a crucial role in generating electrical energy from various sources, including fossil fuels, nuclear reactions, hydroelectric dams, wind turbines, and solar panels. These devices utilize the principles of electromagnetic induction to convert mechanical energy into electrical energy. This process involves rotating a coil of wire within a magnetic field to produce an electrical current.
- Substations serve as essential components of the electrical grid, acting as intermediary points that facilitate voltage level transformations, circuit switching, and the interconnection of different grid segments. Within substations, various critical components are housed, including transformers, circuit breakers, and switches. These components are responsible for modifying voltage levels, redirecting electricity, and ensuring the safe and efficient flow of power within the grid.
- Transmission lines are responsible for transporting high-voltage electricity over long distances, connecting power generation sources to substations located closer to population centers. To minimize energy losses during transmission, these lines operate at high voltages, which reduce current and resistive losses. They are typically constructed using durable materials capable of supporting the weight of the conductors across lengthy spans.
- Distribution lines play a vital role in delivering electricity from substations to homes, businesses, and other end users. Operating at lower voltage levels compared to transmission lines, distribution lines employ transformers to further decrease voltage, ensuring safe electricity distribution in residential and commercial areas.
- Service transformers are strategically placed on utility poles or within pad-mounted enclosures near homes and businesses. These transformers serve the purpose of further reducing voltage from distribution lines to levels suitable for individual consumers. Service transformers consist of a primary winding connected to the distribution line and a secondary winding that provides the appropriate voltage required for powering buildings and appliances.
- The term
loadrefers to the electrical appliances, equipment, and devices that consume electricity in homes, businesses, and industrial settings. Loads are responsible for converting electrical energy into various forms of work, such as lighting, heating, cooling, mechanical motion, or electronic functions, to meet the diverse needs of consumers.

A smart grid is a modern electrical grid system that incorporates digital technology, communication, and automation to enhance the efficiency, reliability, and sustainability of electricity generation, distribution, and usage. It includes elements such as smart meters, distribution boards, renewable energy sources, and real-time data monitoring to optimize grid operations, minimize energy waste, and improve overall grid performance. Smart grids enable more effective management of electricity supply and demand, facilitate the integration of renewable energy sources, and bolster reliability through self-healing mechanisms.
A substation plays a crucial role in the electrical generation, transmission, and distribution system. It performs essential functions, including voltage conversion from high to low (or vice versa) and the conversion of alternating current to direct current or direct current to alternating current. As electric power travels from the generating station to the end consumer, it often passes through multiple substations, each operating at different voltage levels.
These substations may incorporate transformers to facilitate voltage conversion between the high transmission voltages used for long-distance power transport and the lower distribution voltages suitable for homes and businesses. Additionally, substations may also serve as points of connection between two distinct transmission voltage systems. They are an integral and widely prevalent part of our electrical infrastructure.

As shown in the figure above, the components of a substation are as follows:
A. Primary Power Lines' SideB. Secondary Power Lines' Side1. Primary Power Lines2. Ground Wire3. Overhead Lines4. Transformer for Measurement of Electric Voltage5. Disconnect Switch6. Circuit Breaker7. Current Transformer8. Lightning Arrester9. Main Transformer10. Control Building11. Security Fence12. Secondary Power Lines
- Step-up Transmission Substation: These substations are positioned near power generation facilities and play a crucial role in the electrical grid. They receive electrical power generated at nearby facilities and employ large power transformers to elevate the voltage significantly. This elevated voltage is essential for efficient long-distance transmission to supply power to distant locations.
- Step-down Transmission Substation: Positioned strategically throughout the electrical grid, these substations serve as vital junction points. They connect various segments of the grid and act as sources for subtransmission lines. Their primary function is to lower the high voltage received from step-up substations to a level suitable for further distribution within the grid.
- Distribution Substation: Situated in proximity to end-users, distribution substations serve a critical role in delivering electricity to homes and businesses. They are equipped with distribution substation transformers that reduce the voltage from subtransmission levels to levels suitable for consumption by end-users. These substations are responsible for the final stage of electricity distribution before it reaches individual customers.
- Underground Distribution Substation: Similar in function to standard distribution substations, underground distribution substations are also located near end-users. These substations are specifically designed to be situated underground or in urban areas with limited space. They perform the crucial task of reducing subtransmission voltage to levels suitable for end-users, ensuring a reliable and safe power supply.
A circuit breaker is a crucial component in electrical systems. Its primary purpose is to protect electrical circuits from damage caused by overcurrent conditions, such as short circuits or overloads. In short, a circuit breaker serves the following key functions:
- It opens the circuit to interrupt the flow of current when an abnormal or dangerous condition is detected.
- It prevents overheating and potential fires by disconnecting power when necessary.
- It can be manually controlled to open or close the circuit for maintenance or safety reasons.
- In smart grids, it may have communication capabilities for remote monitoring and control.
Modbus is a widely adopted communication protocol, particularly renowned in the realm of industrial automation. It plays a pivotal role in substation communication, facilitating tasks like remote monitoring and control. Modbus exhibits versatility by supporting an array of networking technologies, including both serial communication and TCP/IP enhancements.
Though it excels in serial data communication, Modbus is not finely-tuned for high-speed Ethernet communication. However, there is a specialized variant called Modbus Plus that has been refined to meet the demands of remote communication in industrial environments.
To make Modbus suitable for Internet communication, a solution exists in the form of Modbus/TCP. This technology encapsulates Modbus frames within TCP frames, enabling seamless communication over the Internet.
One key limitation of the Modbus protocol is its lack of support for time-stamped events and polled reports by exception. This can be a hindrance when real-time data tracking and conditional reporting are crucial elements of the communication system.
DNP3, or the Distributed Network Protocol, stands as a protocol stack crucial for communication within automation systems, with a notable emphasis on the power industry and SCADA systems. Its primary application lies in facilitating the interconnection of Intelligent Electronic Devices (IEDs) within substations.
Compared to Modbus, DNP3 is not as widely adopted in industries beyond the power and automation sectors. This protocol adopts a frame structure akin to IEC 60870-5, albeit with some notable distinctions, including the incorporation of CRC checking.
Operatively, DNP3 typically functions at the data link layer (Layer 2) in the OSI model. This strategic placement enables it to offer an array of essential features, including multiplexing, error checking, link control, and data fragmentation.
A key advantage of DNP3 is its efficiency in transporting data within substation communication networks. Its robust capabilities and compatibility with substation-specific applications make it a valuable choice for these critical systems, where reliable and efficient data exchange is of paramount importance.
IEC 61850 defines a hierarchy consisting of three distinct levels:
- Process Level: At this level, various devices such as switchgears, including circuit breakers, switches, current transformers, and voltage transformers, are located. The Process Level forms the foundation of the IEC 61850 hierarchy.
- Bay Level: The Bay Level is home to Intelligent Electronic Devices (IEDs). IEC 61850 introduces the concept of a process bus at this level, facilitating communication between IEDs and intelligent instruments and switchgears. This enables efficient data exchange within the substation.
- Station Level: The Station Level comprises SCADA (Supervisory Control and Data Acquisition) and HMI (Human-Machine Interface) systems. These systems are essential for substation control and monitoring. To interact with IEDs located at the Bay Level, the Station Level utilizes a station bus, ensuring seamless communication and coordination across the entire substation.

-
Layer 1: Process Level
-
Relay House: At the heart of the substation's Layer 1 is the relay house, also known as the protection and control room. This critical component houses Intelligent Electronic Devices (IEDs) responsible for monitoring and protecting substation equipment. Key components within the relay house include:
- Protection Relays: These devices are tasked with monitoring electrical parameters and executing protection functions. Examples include overcurrent protection relays and differential protection relays.
-
Sensors: Positioned strategically within the relay house, sensors such as Current Transformers (CTs) and Voltage Transformers (VTs) measure critical electrical parameters like current and voltage. They provide essential data to IEDs for analysis:
- Current Transformers (CTs): Measure current flow in circuits.
- Voltage Transformers (VTs): Measure voltage levels.
- Communication Interfaces: IEDs within the relay house are equipped with communication interfaces, typically Modbus or DNP3, to relay status and measurement data.
- Transformers: Transformers are a fundamental component of the Process Level, responsible for adjusting voltage levels as required.
-
Relay House: At the heart of the substation's Layer 1 is the relay house, also known as the protection and control room. This critical component houses Intelligent Electronic Devices (IEDs) responsible for monitoring and protecting substation equipment. Key components within the relay house include:
-
Layer 2: Bay Level
- Bay Controllers: Bay controllers are pivotal in supervising and controlling equipment within specific bays of the substation. They maintain communication with IEDs in the Process Level using protocols such as Modbus or DNP3 for seamless data exchange. Additionally, Bay controllers support IEC 61850 communication for advanced applications. A Bay controller can take the form of a single device or a combination of devices tailored to monitor and control a particular bay. Depending on the bay's complexity and the substation's needs, a Bay controller might encompass a Bay Control Unit (BCU) or a Bay Protection and Control Unit (BPCU).
-
Switchgear: Switchgear includes circuit breakers, disconnect switches, and associated control mechanisms. Bay controllers effectively oversee the operation of switchgear, ensuring that equipment is isolated or connected as required based on signals from IEDs.
- Circuit Breakers: These devices are used to open and close electrical circuits. Some circuit breakers may incorporate dedicated controllers.
-
Layer 3: Station Level
- Station Gateway: Serving as the central hub for communication within the substation, the station gateway collects data from multiple bay controllers and IEDs using Modbus or DNP3. It can also support IEC 61850 for station-level control and monitoring.
- Human-Machine Interface (HMI): The HMI provides operators with a graphical interface for real-time monitoring and control of the entire substation. It communicates with the station gateway, offering access to crucial data, alarms, and control options.
-
Network Communication:
- Modbus and DNP3 protocols primarily facilitate communication between devices in the process level and bay level, ensuring smooth data exchange.
- IEC 61850, on the other hand, is employed for advanced substation automation and control, primarily at the station level and between bay controllers and the station gateway. This standard enhances interoperability and advanced functionalities in the substation.
While Internet protocol structures offer secure data transmission, they may not always meet the speed requirements of real-time systems. To address this issue, IEC 61850 standardizes various protocols tailored for different applications:
- MMS (Manufacturing Messaging Specification): MMS is widely employed for facilitating communication between Intelligent Electronic Devices (IEDs) and SCADA systems. It serves as the backbone for exchanging application-specific, configuration, and monitoring data.
- GOOSE (Generic Object-Oriented Substation Events): GOOSE plays a vital role in transmitting status-related messages between IEDs. This protocol is frequently utilized for teleprotection applications, ensuring rapid tripping of protective devices when necessary.
- SMV (Sampled Measured Values): SMV is designed for the swift and dependable communication of measurement, protection, and control values within power systems. It primarily handles data originating from Current Transformers (CT) and Voltage Transformers (VT), enhancing situational awareness and control.
Why Do We Need It?
Correctness is extremely important. Notable incidents like the Therac-25 Radiation Overdosing in 1985-87, the 1994 Intel FDIV (floating point division unit) issue, and the Ariane 5 Crash in 1996 emphasize the criticality of this aspect.
-
Goal: Does the system exhibit the desired behavior? The primary objective is to ensure that the system adheres to the following criteria:
- Undesirable events never occur.
- Desired outcomes are eventually achieved.
-
Analysis Techniques:
- Mathematical Verification: This involves constructing a mathematical model of the system and rigorously proving that it demonstrates the desired characteristics. While this method is highly accurate, it lacks scalability and is prone to errors.
- Peer Review: This static technique relies on manual code inspection without software execution. However, it may struggle to identify subtle errors, especially those related to concurrency and algorithm defects, and it can be costly.
-
Testing: Testing analyzes the system's behavior under specific test cases to infer important properties. It is user-friendly and effective in catching flaws but may fall short in detecting rare or obscure issues and can be time-consuming.
Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. --- Edsger W. Dijkstra - Formal Verification: This bridges the gap between mathematical verification and testing. It offers a level of precision equivalent to a mathematical proof but is not as straightforward to implement as testing.
Specification is the process of precisely describing a system and its desired properties using a language with mathematically defined syntax and semantics. These properties can include functional behavior, timing behavior, performance characteristics, and internal structure. Formal specification is most successful for behavioral properties and is achieved through various methods that focus on sequential or concurrent systems. The main benefits of specification are gaining a deeper understanding of the system, uncovering design flaws, and providing a communication tool between stakeholders. Additionally, the formal specification itself can be analyzed and used to derive properties of the system.
Verification is the process of formally analyzing a system to ensure that it behaves as intended and satisfies its specified properties. Two common methods for verification are model checking and theorem proving.
Design by Contract (DbC) is a software design approach that uses formal contracts to specify expected behavior. These contracts include preconditions, postconditions, and invariants. DbC ensures clients meet preconditions, and if not, the server reports errors. It encourages failing hard for easier debugging. Contracts are documented and enhance code reuse. In practice, contract checks are often disabled in production for performance. DbC complements software testing by providing internal self-tests for early error detection.

Failing hard is a concept in software development that means a program or component should immediately and clearly report an error or failure when it encounters a problem or a condition that violates its expectations (such as contract preconditions). Instead of trying to continue or gracefully handle an error, it crashes, throws an exception, or asserts the error, making the issue unmistakably visible. This approach is favored in Design by Contract (DbC) to simplify debugging and ensure that contract conditions are not violated.
Model checking involves building a finite model of a system and checking if a desired property holds in that model. It performs an exhaustive state space search, ensuring termination due to the finite nature of the model. This method is widely used in hardware and protocol verification and is increasingly applied to software systems.
-
Method: Systematic verification of
$P$ in all states. -
Tools: Model checkers (e.g.,
Spin,NuSMV,Uppaal, etc.). -
Pros:
- Automation: It is highly automated and rapid, often delivering results within minutes.
- Counterexamples: It generates counterexamples when properties are violated, facilitating debugging and identifying design flaws.
- Partial Specifications: It can validate partial specifications, providing insights into system correctness even when not fully specified.
- Wide Applicability: Model checking is widely used in hardware and protocol verification and is increasingly utilized for software system specifications.
-
Cons:
- State Explosion: Dealing with extensive state spaces can be challenging, limiting its utility for complex systems.
- Resource-Intensive: Despite optimizations such as binary decision diagrams and abstraction techniques, it can still demand significant computational resources for very large systems.

In the context of model checking, it is essential to address three fundamental questions:
- Modeling: How should we represent the system?
- Specification: What is the required behavior of the system or program?
- Verification: Why does the system exhibit a particular behavior or, conversely, why does it not?













Theorem proving treats both the system and its desired properties as mathematical formulas expressed in some formal logic. It relies on formal systems with axioms and inference rules to construct a proof that the properties hold. Theorem proving can handle infinite state spaces and requires interaction in interactive systems but provides insights into system correctness.
-
Method: Provide a formal proof that
$P$ holds. -
Tools: Theorem prover/proof assistant or proof checker (e.g.,
Coq,Isabelle/HOL,ACL2, etc.). -
Pros:
- Expressiveness: Theorem proving can address intricate and expressive properties since it is grounded in formal logic and mathematical reasoning.
- General Applicability: It is suitable for a broad spectrum of systems, encompassing both software and hardware.
- Soundness and Completeness: When a property is proven, it guarantees correctness.
- Formal Verification: It is frequently employed for critical systems where ensuring correctness is paramount.
-
Cons:
- Complexity: Theorem proving can be a laborious and time-consuming process, especially for intricate systems and properties.
- Manual Involvement: It often necessitates expert knowledge and manual guidance for the development of formal proofs, making it labor-intensive.
- Limited Automation: Unlike model checking, theorem proving is not entirely automated and may not yield results as swiftly.





Formal verification and validation techniques play a pivotal role in ensuring the correctness and reliability of both software and hardware systems. These techniques can be categorized in terms of their formality and hierarchy:
- Contract-Based Formal Methods specify system behavior using contracts, which define preconditions and postconditions. These methods provide clear interfaces and expectations, though they are relatively less formal. They are typically used during the design and coding phases to ensure compliance with the established contracts.
- Model Checking involves creating a mathematical model and exhaustively checking it against specified properties. This approach is especially suitable for systems with finite state spaces and is more formal than contract-based methods. It automates property verification, but it may encounter challenges related to state-space explosion.
- Theorem Proving is the most formal technique, employing formal logic and mathematics for rigorous verification. This approach is particularly well-suited for complex and critical systems. It involves manual or interactive proofs, ensuring high precision but potentially being labor-intensive.
Contract-based methods are typically employed during the design and coding phases to establish specifications. Model checking is applied to systems with manageable state spaces, primarily focusing on specific property checks. Theorem proving is reserved for critical systems or complex cases that demand the highest level of assurance. It is worth noting that these techniques are not mutually exclusive and can be used in combination, depending on the specific requirements and constraints of a given project.
-
Specification Languages:
- Z notation: A formal specification language that uses mathematical notation to describe system requirements.
- VDM (Vienna Development Method): A method and notation for specifying software systems using mathematical constructs.
-
Modeling and Specification Tools:
- UML (Unified Modeling Language): A standard modeling language for visualizing, specifying, constructing, and documenting the artifacts of software systems.
- Alloy: A lightweight modeling language for software design and analysis.
-
Theorem Provers and Proof Assistants:
- Coq: An interactive proof assistant that allows the development of formal mathematical proofs and certified software.
- Isabelle/HOL: A generic proof assistant with a higher-order logic for formal proof development.
-
Model Checkers:
- Spin: A model checker used for verifying correctness properties of concurrent and distributed systems.
- NuSMV: A model checker for the verification of finite state systems.
-
Static Analysis Tools:
- PVS (Prototype Verification System): A theorem prover and specification language for formal verification.
- Frama-C: A framework for the analysis of C programs, with support for formal verification.
-
Runtime Verification Tools:
- Java PathFinder: A runtime verification tool for Java programs, used to find defects and verify properties.
- LTL (Linear Temporal Logic): Tools for runtime verification of temporal logic properties in reactive systems.
-
Automated Testing and Property-Based Testing Tools:
- QuickCheck: A property-based testing tool for Haskell and other programming languages.
-
SAT and SMT Solvers:
- Z3: A popular Satisfiability Modulo Theories (SMT) solver used in formal methods and program analysis.
- MiniSat: A minimalistic, open-source SAT solver.
-
Type Systems:
- Haskell and GHC (Glasgow Haskell Compiler): A functional programming language and its compiler with advanced type system features.
- Ada and SPARK: Programming languages designed for safety-critical and high-integrity systems, with strong type systems.
-
Program Analysis Tools:
- ESBMC (Explicit-State Bitstate Model Checker): A model checker for software that uses a bit-precise approach for verification.
-
Formal Specification and Verification Frameworks:
- TLA+: A specification language and model checker for system-level specifications.
- Event-B: A formal method for system-level modeling and verification.
-
Refinement and Transformation Tools:
- Rigorous System Design (RSD): A framework for systematic refinement and development of software and hardware systems.
Active Notebooks
- Aditi Kulkarni's Notebook
- Aly Aadil Salewala's Notebook
- Carter Pattison's Notebook
- Christopher Gossmann's Notebook
- Esha Pansara's Notebook
- Estelle Jung's Notebook
- Favour Adekola's Notebook
- Galadriel Cho's Notebook
- Prisha Baravkar's Notebook
- Rishika Vunnama's Notebook
- Ryosuke Shibuya's notebook
- Txaber Trevino's Notebook
- Zeus Banda's Notebook
Archive
- Adam McAndrews Notebook
- Albert Nguyen Notebook
- Alexander Rice's Notebook
- Amani Bedwa's Notebook
- Aparupa Brahma's Notebook
- Arya Gujarathi's Notebook
- Bermet Talantbekova's Notebook
- Calvin Rioux's Notebook
- Christina Shih Notebook
- Chungman Kim's NoteBook
- Connor McCary's Notebook
- Dhruv Patels Virtual Notebook
- Elliot Kantor's Notebook
- Ethan Lee Notebook
- Filippos Notebook
- Gweneth Smith's Notebook
- Hubert Pan's Notebook
- Hussein Rmaile Notebook
- Isabella Jemal's Notebook
- Joseph Masson's Notebook
- Jude Karaki Notebook
- Kaden McCartney's Notebook
- Maria Cymbalyuk's Notebook
- Natalie Ajemian's Notebook
- Nguyen Nguyen's Notebook
- Nicholas Reed's NoteBook
- Piper Wright's Notebook
- Quintin's notebook
- Rahil's Notebook
- Raj Patel Notebook
- Reva Hajarnis Notebook
- Rick Berglund's Notebook
- Rossy's Notebook
- Sabina Sokol's Notebook
- Safiy Malik Notebook
- Sam Ling's Notebook
- Sam Litchfield Example Notebook
- Shrayes Upadhyayula Notebook
- Soyoung Moon's Notebook
- Suraj Shekar Notebook
- Vidur Modgil's Notebook
- Xin Zhao Notebook
- Xinyan(Rose) Jiang's Notebook
- Zaeem Ahmad Notebook