Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

Multimachine Stability

Multimachine Stability

Multimachine stability analysis is crucial for understanding the dynamics and stability of power systems with multiple synchronous machines. The objective is to solve the swing equations for a network of M machines connected to an N-bus power system.
In analyzing the system, the nodal equations represent the relationship between bus voltages, machine voltages, and machine currents. The nodal equation is given by:

The Power Flow Problem and Solution

The Power Flow Problem and Solution

Power flow problem analysis is fundamental for determining real and reactive power flows in network components, such as transmission lines, transformers, and loads. The power system's single-line diagram provides data on the bus, transmission line, and transformer. Each bus k in the system is characterized by four key variables: voltage magnitude Vk, phase angle δk, real power Pk, and reactive power Qk. Two of these four variables are inputs, while the...

Circuit Terminology

Circuit Terminology

An electrical network is a system composed of interconnected elements, such as resistors, capacitors, inductors, and voltage or current sources. Unlike a circuit, an electrical network does not necessarily form a closed path. In other words, while all circuits can be considered networks due to their interconnected nature, not every network qualifies as a circuit.
A circuit, on the other hand, is also an interconnected system of electrical elements but must contain one or more closed paths.

Simplified Synchronous Machine Model

Simplified Synchronous Machine Model

The Synchronous Machine Model is a fundamental tool in analyzing and ensuring the transient stability of power systems. This model simplifies the representation of a synchronous machine under balanced three-phase positive-sequence conditions, assuming constant excitation and ignoring losses and saturation. The model is pivotal for understanding the behavior of synchronous generators connected to a power grid, particularly during transient events.
In this model, each generator is connected to a...

Transformers with Off-Nominal Turns Ratios

Transformers with Off-Nominal Turns Ratios

In scenarios involving parallel transformers with disparate ratings, developing per-unit models requires accommodating off-nominal turns ratios. This situation arises when the selected base voltages are not proportional to the transformer’s voltage ratings. Consider a transformer where the rated voltages are related by the term a. If the chosen voltage bases satisfy a relationship involving term b, term c is defined as the ratio of these bases. This ratio is then substituted into the...

Mesh Analysis for AC Circuits

Mesh Analysis for AC Circuits

In the domain of radio communication, the significance of impedance matching must be considered. It is crucial to ensure the efficient transmission of signals between radio transmitters and receivers. Achieving this balance involves using impedance-matching circuits, with one fundamental configuration comprising a resistor, capacitor, and inductor.
The process of harmonizing these impedances begins with a clear understanding of the input and output signals. Once these signals are known, the...

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by

Same author

A Systematic Review on the Applications of Uppaal.

Sensors (Basel, Switzerland)·2025

Same author

Intelligent Industrial Process Control Systems.

Sensors (Basel, Switzerland)·2023

Same author

Determinism in Cyber-Physical Systems Specified by Interpreted Petri Nets.

Sensors (Basel, Switzerland)·2020

Same author

Formal Verification of Control Modules in Cyber-Physical Systems.

Sensors (Basel, Switzerland)·2020

Search research articles

Related Experiment Video

Updated: Aug 27, 2025

A Rapid Method for Modeling a Variable Cycle Engine

A Rapid Method for Modeling a Variable Cycle Engine

Published on: August 13, 2019

Model Checking Autonomous Components within Electric Power Systems Specified by Interpreted Petri Nets.

Iwona Grobelna¹, Paweł Szcześniak¹

¹Institute of Automatic Control, Electronics and Electrical Engineering, University of Zielona Góra, 65-516 Zielona Góra, Poland.

Sensors (Basel, Switzerland)

|September 23, 2022

Summary

Formal verification of autonomous electric power systems using interpreted Petri nets ensures safety and liveness. This method identifies design errors early by checking user-defined properties with the nuXmv model checker.

Keywords:

Petri net control system model checking power energy system specification verification

More Related Videos

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

Published on: June 1, 2022

Finite Element Modelling of a Cellular Electric Microenvironment

Finite Element Modelling of a Cellular Electric Microenvironment

Published on: May 18, 2021

Related Experiment Videos

Last Updated: Aug 27, 2025

A Rapid Method for Modeling a Variable Cycle Engine

A Rapid Method for Modeling a Variable Cycle Engine

Published on: August 13, 2019

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

Published on: June 1, 2022

Finite Element Modelling of a Cellular Electric Microenvironment

Finite Element Modelling of a Cellular Electric Microenvironment

Published on: May 18, 2021

Area of Science:

Electrical Engineering
Computer Science
Formal Methods

Background:

Autonomous components in electric power systems require rigorous specification and verification.
Interpreted Petri nets offer a formal method for specifying system behavior.
Ensuring safety and liveness properties is critical for reliable power system operation.

Purpose of the Study:

To present a formal method for verifying user-defined behavioral properties of autonomous electric power system components.
To demonstrate the application of interpreted Petri nets and temporal logic for formal verification.
To enable early identification of design errors in autonomous power system components.

Main Methods:

Specification of autonomous components using interpreted Petri nets.
Transformation of interpreted Petri nets into rule-based logical models.
Formal verification of system properties using temporal logic formulas and the nuXmv model checker.
Application to an electric energy storage (EES) system for stabilizing renewable energy sources (RES).

Main Results:

Interpreted Petri nets can be formally verified against user-defined safety and liveness properties.
The proposed method allows for automatic checking of system requirements.
Design errors in autonomous components can be detected at an early stage.
The approach was successfully applied to an EES control algorithm.

Conclusions:

Formal verification using interpreted Petri nets and temporal logic is effective for ensuring the safety and liveness of autonomous electric power systems.
This methodology facilitates early detection of design flaws, improving system reliability.
The presented approach provides a robust framework for specifying and verifying complex control algorithms in power systems.