Formal verification and quantitative metrics of MPSoC data dynamics

DOI10.1007/S00165-017-0444-0MaRDI QIDQ1707342zbMATH OpenOpenAlexFDO

Authors 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

hybrid automataprobabilistic timed automataformal verificationMPSoCdata dynamicsreach-ratio metric

Mathematics Subject Classification ID

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

Recommendations

• Models and formal verification of multiprocessor system-on-chips
• Communication mechanism designed for distributed intrusion detection system
• scientific article; zbMATH DE number 1390911
• Allocation and Scheduling for MPSoCs via Decomposition and No-Good Generation
• Stochastic allocation and scheduling for conditional task graphs in multi-processor systems-on-chip

Cites work

• scientific article; zbMATH DE number 1696496 (Why is no real title available?)
• scientific article; zbMATH DE number 1196650 (Why is no real title available?)
• scientific article; zbMATH DE number 1303063 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 2090709 (Why is no real title available?)
• Algorithmic analysis of nonlinear hybrid systems
• Automated Technology for Verification and Analysis
• Automatic verification of real-time systems with discrete probability distributions.
• Differential dynamic logic for hybrid systems
• Ellipsoidal Techniques for Reachability Analysis of Discrete-Time Linear Systems
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Models and formal verification of multiprocessor system-on-chips
• Monte Carlo optimisation for conflict resolution in air traffic control
• Non-linear loop invariant generation using Gröbner bases
• Performance analysis of probabilistic timed automata using digital clocks
• Reachability Analysis of Hybrid Systems Using Support Functions
• Stochastic games for verification of probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Temporal verification of reactive systems: response

Cited in

(2)

• Models and formal verification of multiprocessor system-on-chips
• Communication mechanism designed for distributed intrusion detection system

Describes a project that uses

Uses Software

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

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

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