Logo - springer
Slogan - springer

Computer Science - Theoretical Computer Science | Formal Modeling and Analysis of Timed Systems - 5th International Conference, FORMATS 2007, Salzburg,

Formal Modeling and Analysis of Timed Systems

5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings

Raskin, Jean-Francois, Thiagarajan, P.S. (Eds.)

2007, X, 372 p.

Available Formats:

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.


(net) price for USA

ISBN 978-3-540-75454-1

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase

learn more about Springer eBooks

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-3-540-75453-4

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items

This book constitutes the refereed proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007, held in Salzburg, Austria, in October 2007.

The 22 revised full papers presented together with three invited talks were carefully reviewed and selected from 48 submissions. The papers cover work on foundations and semantics of timed systems including timed automata, timed Petri nets, hybrid automata, timed process algebra, max-plus algebra, and probabilistic models. There are contributions on techniques, algorithms, data structures, and software tools for analyzing timed systems and resolving temporal constraints such as scheduling, worst-case execution time analysis, optimization, model-checking, testing, and constraint solving. In addition, there are also articles on applications like real-time software, hardware circuits, and problems of scheduling in manufacturing and telecommunication.

Content Level » Research

Keywords » Algorithms - Automat - algorithm - automata - data structure - data structures - modeling - optimization - petri net - real-time - semantics - tools

Related subjects » Communication Networks - Software Engineering - Theoretical Computer Science

Table of contents 

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.

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Logics and Meanings of Programs.