Formal Modeling and Analysis of Timed Systems

Abstraction of Probabilistic Systems.- From Analysis to Design.- Efficient On-the-Fly Algorithms for Partially Observable Timed Games.- Undecidability of Universality for Timed Automata with Minimal Resources.- On Timed Models of Gene Networks.- Costs Are Expensive!.- Hypervolume Approximation in Timed Automata Model Checking.- Counter-Free Input-Determined Timed Automata.- Towards Budgeting in Real-Time Calculus: Deferrable Servers.- Automatic Abstraction Refinement for Timed Automata.- Dynamical Properties of Timed Automata Revisited.- Robust Sampling for MITL Specifications.- On the Expressiveness of MTL Variants over Dense Time.- Quantitative Model Checking Revisited: Neither Decidable Nor Approximable.- Efficient Detection of Zeno Runs in Timed Automata.- Partial Order Reduction for Verification of Real-Time Components.- Guided Controller Synthesis for Climate Controller Using Uppaal Tiga.- Symbolic Reachability Analysis of Lazy Linear Hybrid Automata.- Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters.- Multi-processor Schedulability Analysis of Preemptive Real-Time Tasks with Variable Execution Times.- Designing Consistent Multimedia Documents: The RT-LOTOS Methodology.- AMT: A Property-Based Monitoring Tool for Analog Systems.- Region Stability Proofs for Hybrid Systems.- CSL Model Checking Algorithms for Infinite-State Structured Markov Chains.- Symbolic Simulation-Checking of Dense-Time Automata.