Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar
This report details the translation and testing of multiple benchmarks, including the Six Vehicle Platoon, Two Bouncing Ball, Three Tank System, and Four-Dimensional Linear Switching, which represent continuous and hybrid systems. These benchmarks were gathered from past instances involving diverse verification tools such as SpaceEx, Flow*, HyST, MATLAB-Simulink, Stateflow, etc. They cover a range of systems modeled as hybrid automata, providing a comprehensive set for analysis and evaluation. Initially, we created models for all four systems using various suitable tools. Subsequently, these models were converted to the SpaceEx format and then translated into different formats compatible with various verification tools. Adapting our approach to the dynamic characteristics of each system, we performed reachability analysis using the respective verification tools.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata
Simulink is widely used in industrial design processes to model increasingly complex embedded control systems. Thus, their formal analysis is highly desirable. However, this comes with two major challenges: First, Simuli…
SIM-CE: An Advanced Simulink Platform for Studying the Brain of Caenorhabditis elegans
We introduce SIM-CE, an advanced, user-friendly modeling and simulation environment in Simulink for performing multi-scale behavioral analysis of the nervous system of Caenorhabditis elegans (C. elegans). SIM-CE contains…
Stability in Isolated Grids: Implementation and Analysis of the Dead-Zone Virtual Oscillator Control in Simulink and Typhoon HIL
This paper explores the analysis and implementation of the Virtual Oscillator Control (VOC) strategy for inverters aiming to enhance stability amidst the ever-increasing generation of renewable energy sources like solar …
Breaking the Limits of Redundancy Systems Analysis
Redundancy mechanisms such as triple modular redundancy protect safety-critical components by replication and thus improve systems fault tolerance. However, the gained fault tolerance comes along with costs to be investe…
Laser Doppler vibrometer and accelerometer for vibrational analysis of the automotive components during Simulink simulation for validation
In current research, laser Doppler vibrometer (LDV) as a new diagnostic tool is utilized for non-destructive testing of the automotive equipment. LDV technique is working based on measurement of the Doppler shift of a mo…
Diagnostic