Models and formal verification of multiprocessor system-on-chips

DOI10.1016/J.JLAP.2008.05.002MaRDI QIDQ953526zbMATH OpenOpenAlexWikidataFDO

Authors Michael R. Hansen, Jan Madsen, Aske W. Brekling

Publication date 6 November 2008

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2008.05.002

zbMATH Keywords

verificationtimed automataschedulabilitymultiprocessor system-on-chipsuppaal

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal verification of multitasking applications based on timed automata model
• Publication:4935948
• Formal verification and quantitative metrics of MPSoC data dynamics
• Multiprocessor extensions to real-time calculus
• scientific article; zbMATH DE number 5046457

Cites work

• scientific article; zbMATH DE number 2080041 (Why is no real title available?)
• scientific article; zbMATH DE number 2080067 (Why is no real title available?)
• scientific article; zbMATH DE number 1796155 (Why is no real title available?)
• A theory of timed automata
• Bounds on Multiprocessing Timing Anomalies
• Formal Methods for the Design of Real-Time Systems
• Formal Modeling and Analysis of Timed Systems
• Scheduling with timed automata
• Uppaal in a nutshell
• Verification of the legOS scheduler using Uppaal

Cited in

(7)

• A formal method for determining the state of processors in a multiprocessor system under testing
• Model Checking Real-Time Systems
• A hybrid performance analysis technique for distributed real-time embedded systems
• scientific article; zbMATH DE number 5046457 (Why is no real title available?)
• Specification and verification of a MPI implementation for a MP-SoC
• Research and Development of an Algorithm for the Response Time Estimation in Multiprocessor Systems Under the Interval Uncertainty of the Tasks Execution Times
• Formal verification and quantitative metrics of MPSoC data dynamics

Describes a project that uses

Uses Software

• TIMES
• SPIN
• Uppaal
• legOS

This page was built for publication: Models and formal verification of multiprocessor system-on-chips

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