On checking equivalence of simulation scripts

DOI10.1016/J.JLAMP.2021.100640MaRDI QIDQ2035653zbMATH OpenOpenAlexFDO

Authors Toni Mancini, Federico Mari, A. Massini, Igor Melatti, Enrico Tronci

Publication date 25 June 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2021.100640

zbMATH Keywords

formal verificationformal verification of cyber-physical systemssimulation based formal verificationsystem-level formal verification

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Simulator semantics for system level formal verification
• On minimising the maximum expected verification time
• SyLVaaS: system level formal verification as a service
• Simulink timed models for program verification
• Hybrid Systems: Computation and Control

Cites work

• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 1182386 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• HyTech: A model checker for hybrid systems
• Linearizing Discrete-Time Hybrid Systems
• Model-based testing of reactive systems. Advanced lectures.
• Mutation-Based Test Case Generation for Simulink Models
• Numerical nonlinear regulator design
• On minimising the maximum expected verification time
• On simulation-based probabilistic model checking of mixed-analog circuits
• S-TaLiRo: a tool for temporal logic falsification for hybrid systems
• Simulation-equivalent reachability of large linear systems with inputs
• Simulator semantics for system level formal verification
• SyLVaaS: system level formal verification as a service
• Towards a UTP semantics for Modelica

Cited in

(5)

• Editorial: Tribute to Anna Labella
• Refinement checking based on simulation relations
• SyLVaaS: system level formal verification as a service
• Simulator semantics for system level formal verification
• Theory of Cryptography

Describes a project that uses

Uses Software

• StateFlow
• AutoMOTGen
• S-TaLiRo
• dReach
• PHAVer
• HyTech
• Uppaal
• Dymola
• DryVR

This page was built for publication: On checking equivalence of simulation scripts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2035653)