PV2 ⊧ SAW: Safety Analysis of Weakly-hard Systemsgenerates several safe regions of weakly hard system

Application domain/field

• Weakly-hard systems
• Safety verification

Expected input

Model file that specifies

• Dynamic system $f$
• Sampling period $\delta$
• Safe state region $X$
• Weakly-hard constraint $(m,K)$
• Control law $\pi$

Optional: Configuration file of Flow*. This is set by default but can be customized.

Expected output

• $X_s$: Safe initial set
• ${\Gamma }_S$: Largest set from which the system will not leave the safe region.
• ${\Gamma }_I$: Largest subset of ${\Gamma }_S$ that satisfies the inductiveness

Internals

SAW focuses on the analysis of weakly-hard systems. Weakly-hard systems are introduced as systems where deadlines should be met ("hard" systems) though it is allowed to miss an occasional deadline ("weakly"). SAW computes a tight estimation of the safe initial set for infinite-time safety verification of general nonlinear weakly-hard systems.