Verifying distributed real-time properties of embedded systems via graph transformations and model checking

DOI10.1007/S11241-006-6883-YzbMath1103.68630OpenAlexW2068025314MaRDI QIDQ853626

Douglas C. Schmidt, Gabor Madl, Sherif Abdelwahed

Publication date: 17 November 2006

Published in: Real-Time Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11241-006-6883-y

zbMATH Keywords

embedded systemsmodel checkingschedulability analysiscomponent middlewaredistributed real-time

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99)

Uses Software

• Kronos
• VEST
• Uppaal2k
• IF-2.0
• SPIN
• HyTech
• Uppaal
• DREAM Tool
• Ptolemy
• Giotto
• dSPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Model driven middleware: A new paradigm for developing distributed real-time and embedded systems
• Scheduling subject to resource constraints: Classification and complexity
• A theory of timed automata
• Experimental evaluation of state-of-the-art heuristics for the resource-constrained project scheduling problem
• Rate monotonic vs. EDF: judgment day
• Uppaal in a nutshell
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal Methods for the Design of Real-Time Systems
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment

This page was built for publication: Verifying distributed real-time properties of embedded systems via graph transformations and model checking