Formal verification and quantitative metrics of MPSoC data dynamics

DOI10.1007/s00165-017-0444-0zbMath1382.68145OpenAlexW2767475216MaRDI QIDQ1707342

Hui Zhang, Jinzhao Wu

Publication date: 29 March 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0444-0

zbMATH Keywords

formal verificationhybrid automataprobabilistic timed automataMPSoCdata dynamicsreach-ratio metric

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• PRISM
• PHAVer
• HyTech
• RSOLVER
• Benchmarks
• HSolver
• SpaceEx

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Performance analysis of probabilistic timed automata using digital clocks
• Models and formal verification of multiprocessor system-on-chips
• Differential dynamic logic for hybrid systems
• Automatic verification of real-time systems with discrete probability distributions.
• Symbolic model checking for probabilistic timed automata
• Non-linear loop invariant generation using Gröbner bases
• Temporal Verification of Reactive Systems: Response
• Reachability Analysis of Hybrid Systems Using Support Functions
• Stochastic Games for Verification of Probabilistic Timed Automata
• Algorithmic analysis of nonlinear hybrid systems
• Ellipsoidal Techniques for Reachability Analysis of Discrete-Time Linear Systems
• Automated Technology for Verification and Analysis
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control

This page was built for publication: Formal verification and quantitative metrics of MPSoC data dynamics