1st Formal Methods for Timing Verification Workshop

In conjunction with the 19th International Symposium on Formal Methods (FM 2014)

FM 2014 website: http://www.comp.nus.edu.sg/~pat/FM2014/cfp.html

Goals:

The growing complexity of real-time embedded systems creates new challenges for performance evaluation engineering practices: it is namely expected that delivered products implement more and more complex features, while respecting strict real-time requirements. For such systems, an ever-increasing portion of design effort is therefore spent on timing verification. The verification space covering the system timing behavior is likely to be very large making it infeasible to verify each point in this space. Formal timing verification methods and techniques allow tackling this problem by providing formal proofs on an abstract mathematical temporal model of the system. Such temporal models are however rarely used in the industrial design practices, thus requiring additional efforts from the timing verification community to fill the gap between the design model and the temporal model semantics.

The purpose of the FMTV'14 workshop is to share ideas, experiences and solutions to concrete timing verification problems. Industrials are also invited to provide feedbacks on applying formal timing verification techniques in their context. Original unpublished papers on all aspects of formal timing verification for real-time embedded systems are welcome.

The particularity of the FMTV'14 workshop will be the presentation of a challenge to the formal timing verification community with scientific stakes issued from a real industrial case study.

Topics:

Topics include but are not limited to:

• Comparative evaluation of existing formal timing verification algorithms and techniques
• Integration and applicability of formal timing verification techniques in the industrial development practices
• Case studies and industrial experiences using formal timing verification techniques
• Scheduling analysis for real-time, distributed and embedded applications
• Network queuing analysis theory
• End-to-end response time analysis
• Formal methods for WCET computation
• Integration of WCET and scheduling analysis