Formal verification of real-time systems with preemptive scheduling
DOI10.1007/S11241-008-9059-0zbMATH Open1185.68429OpenAlexW2086156607MaRDI QIDQ844238FDOQ844238
Authors: Didier Lime, Olivier H. Roux 
Publication date: 18 January 2010
Published in: Real-Time Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11241-008-9059-0
Recommendations
- Verification, refinement and scheduling of real-time programs
- Verification of schedulability for real-time programs
- Formal verification of discrete real-time systems
- scientific article; zbMATH DE number 49713
- Specification and compositional verification of real-time systems
- Schedule verification and synthesis for embedded real-time components
- Real-Time Systems
Cellular automata (computational aspects) (68Q80) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- HyTech: A model checker for hybrid systems
- Computer Aided Verification
- Title not available (Why is that?)
- A theory of timed automata
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
- Title not available (Why is that?)
- Symbolic model checking for real-time systems
- Title not available (Why is that?)
- The algorithmic analysis of hybrid systems
- Reachability problems and abstract state spaces for time Petri nets with stopwatches
- Applications and Theory of Petri Nets 2004
- Model checking of time Petri nets using the state class timed automaton
- State space computation and analysis of Time Petri Nets
- Schedulability analysis of fixed-priority systems using timed automata
- Scheduler modeling based on the controller synthesis paradigm
- A causal semantic for time Petri nets
- Title not available (Why is that?)
Cited In (9)
- A process algebraic approach to the schedulability analysis and workload abstraction of hierarchical real-time systems
- Verification of schedulability for real-time programs
- Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
- Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets
- TPAP: an algebra of preemptive processes for verifying real-time systems with shared resources
- A game approach to the parametric control of real-time systems
- Verifying weakly-hard real-time properties of traffic streams in switched networks
- Formalizing Real-Time Scheduling Using Priority-Based Supervisory Control of Discrete-Event Systems
- Symbolic unfolding of parametric stopwatch Petri nets
Uses Software
This page was built for publication: Formal verification of real-time systems with preemptive scheduling
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q844238)
