Formal verification of real-time systems with preemptive scheduling

DOI10.1007/S11241-008-9059-0MaRDI QIDQ844238zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

verificationhybrid automataformal methodsPetri netspreemptive scheduling

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 3177183 (Why is no real title available?)
• scientific article; zbMATH DE number 1956583 (Why is no real title available?)
• scientific article; zbMATH DE number 1759608 (Why is no real title available?)
• scientific article; zbMATH DE number 2147037 (Why is no real title available?)
• A causal semantic for time Petri nets
• A theory of timed automata
• Applications and Theory of Petri Nets 2004
• Computer Aided Verification
• HyTech: A model checker for hybrid systems
• Model checking of time Petri nets using the state class timed automaton
• Reachability problems and abstract state spaces for time Petri nets with stopwatches
• Schedulability analysis of fixed-priority systems using timed automata
• Scheduler modeling based on the controller synthesis paradigm
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
• State space computation and analysis of Time Petri Nets
• Symbolic model checking for real-time systems
• The algorithmic analysis of hybrid systems

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

Describes a project that uses

Uses Software

• FAST
• HyTech
• Romeo

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)