Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Linear time-invariant Systems01:23

Linear time-invariant Systems

1.1K
A system is linear if it displays the characteristics of homogeneity and additivity, together termed the superposition property. This principle is fundamental in all linear systems. Linear time-invariant (LTI) systems include systems with linear elements and constant parameters.
The input-output behavior of an LTI system can be fully defined by its response to an impulsive excitation at its input. Once this impulse response is known, the system's reaction to any other input can be...
1.1K
Types of Errors: Detection and Minimization01:12

Types of Errors: Detection and Minimization

12.0K
Error is the deviation of the obtained result from the true, expected value or the estimated central value. Errors are expressed in absolute or relative terms.
Absolute error in a measurement is the numerical difference from the true or central value. Relative error is the ratio between absolute error and the true or central value, expressed as a percentage.
Errors can be classified by source, magnitude, and sign. There are three types of errors: systematic, random, and gross.
Systematic or...
12.0K
BIBO stability of continuous and discrete -time systems01:24

BIBO stability of continuous and discrete -time systems

1.1K
System stability is a fundamental concept in signal processing, often assessed using convolution. For a system to be considered bounded-input bounded-output (BIBO) stable, any bounded input signal must produce a bounded output signal. A bounded input signal is one where the modulus does not exceed a certain constant at any point in time.
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
1.1K
Statically Indeterminate Problem Solving01:16

Statically Indeterminate Problem Solving

849
Statically indeterminate problems are those where statics alone can not determine the internal forces or reactions. Consider a structure comprising two cylindrical rods made of steel and brass. These rods are joined at point B and restrained by rigid supports at points A and C. Now, the reactions at points A and C and the deflection at point B are to be determined. This rod structure is classified as statically indeterminate as the structure has more supports than are necessary for maintaining...
849
Block Diagram Reduction01:22

Block Diagram Reduction

638
The process of deriving the transfer function of a control system often involves reducing its block diagram to a single block. This simplification can be achieved through a series of strategic operations, including relocating branch points and comparators. These operations preserve the overall function of the system while allowing for easier manipulation and combination of blocks.
The first step in this process is the identification and relocation of a branch point. A branch point, where a...
638
Propagation of Uncertainty from Systematic Error01:10

Propagation of Uncertainty from Systematic Error

1.6K
The atomic mass of an element varies due to the relative ratio of its isotopes. A sample's relative proportion of oxygen isotopes influences its average atomic mass. For instance, if we were to measure the atomic mass of oxygen from a sample, the mass would be a weighted average of the isotopic masses of oxygen in that sample. Since a single sample is not likely to perfectly reflect the true atomic mass of oxygen for all the molecules of oxygen on Earth, the mass we obtain from this...
1.6K

You might also read

Related Articles

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

Sort by
Same author

A quasi-stationary distribution bound for fault analysis in gene regulatory networks.

Journal of the Royal Society, Interface·2026
Same author

A Quasi-Stationary Distribution Bound for Fault Analysis in Gene Regulatory Networks.

bioRxiv : the preprint server for biology·2025
Same author

Distributed computing inspired by biology.

Seminars in cell & developmental biology·2025
Same author

MobsPy: A programming language for biochemical reaction networks.

PLoS computational biology·2025
Same author

Phage-mediated intercellular CRISPRi for biocomputation in bacterial consortia.

Nucleic acids research·2024
Same author

An Allee-based distributed algorithm for microbial whole-cell sensors.

NPJ systems biology and applications·2024
Same journal

Preserving provability over GPU program optimizations with annotation-aware transformations.

Formal methods in system design·2025
Same journal

Golem: a flexible and efficient solver for constrained Horn clauses.

Formal methods in system design·2025
Same journal

Predicate abstraction for hyperliveness verification.

Formal methods in system design·2025
Same journal

Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker.

Formal methods in system design·2024
Same journal

Global guidance for local generalization in model checking.

Formal methods in system design·2024
Same journal

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).

Formal methods in system design·2024
See all related articles

Related Experiment Video

Updated: Mar 27, 2026

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly
09:51

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

8.1K

Runtime verification of embedded real-time systems.

Thomas Reinbacher1, Matthias Függer1, Jörg Brauer2

  • 1Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.

Formal Methods in System Design
|January 12, 2016
PubMed
Summary
This summary is machine-generated.

This study introduces a runtime verification framework for monitoring past-time Metric Temporal Logic (ptMTL) specifications in real-time systems. The framework uses efficient, reconfigurable hardware blocks for on-line analysis, improving system reliability.

Keywords:
Embedded real-time systemsOnline monitoringPast-time logicsRuntime verification

More Related Videos

Real-Time Proxy-Control of Re-Parameterized Peripheral Signals using a Close-Loop Interface
11:54

Real-Time Proxy-Control of Re-Parameterized Peripheral Signals using a Close-Loop Interface

Published on: May 8, 2021

5.3K
Technical Aspect of the Automated Synthesis and Real-Time Kinetic Evaluation of [11C]SNAP-7941
09:50

Technical Aspect of the Automated Synthesis and Real-Time Kinetic Evaluation of [11C]SNAP-7941

Published on: April 28, 2019

8.1K

Related Experiment Videos

Last Updated: Mar 27, 2026

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly
09:51

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

8.1K
Real-Time Proxy-Control of Re-Parameterized Peripheral Signals using a Close-Loop Interface
11:54

Real-Time Proxy-Control of Re-Parameterized Peripheral Signals using a Close-Loop Interface

Published on: May 8, 2021

5.3K
Technical Aspect of the Automated Synthesis and Real-Time Kinetic Evaluation of [11C]SNAP-7941
09:50

Technical Aspect of the Automated Synthesis and Real-Time Kinetic Evaluation of [11C]SNAP-7941

Published on: April 28, 2019

8.1K

Area of Science:

  • Computer Science
  • Electrical Engineering
  • Formal Methods

Background:

  • Runtime verification is crucial for ensuring the correctness of embedded real-time systems.
  • Existing methods for monitoring temporal logic specifications can be computationally intensive.
  • Past-time Metric Temporal Logic (ptMTL) offers a powerful way to specify system properties over time.

Purpose of the Study:

  • To develop a novel runtime verification framework for ptMTL specifications.
  • To design efficient, hardware-accelerated observer algorithms for ptMTL modalities.
  • To enable on-line, non-interfering monitoring of embedded real-time systems.

Main Methods:

  • Developed observer algorithms tailored for time-bounded ptMTL operators.
  • Leveraged the parallelism inherent in hardware designs for algorithm optimization.
  • Formally proved the correctness of the observer algorithms.
  • Analyzed the time and space complexity of the algorithms, achieving doubly logarithmic time complexity for the Since operator.

Main Results:

  • The proposed algorithms are translatable into efficient, reconfigurable hardware blocks.
  • The framework supports both prototyping and post-deployment monitoring phases.
  • Achieved doubly logarithmic time complexity for the time-bounded Since operator.
  • Demonstrated the framework's feasibility through implementation on a Field Programmable Gate Array (FPGA).

Conclusions:

  • The runtime verification framework provides an efficient and scalable solution for monitoring ptMTL specifications.
  • The hardware-based approach offers a promising direction for self-contained, non-interfering real-time system monitoring.
  • The framework's reconfigurability enhances its applicability across different stages of the system lifecycle.