In conjunction with FM 2014

1st Formal Methods for Timing Verification Workshop

(FMTV’ 14)

Call for Papers in PDF


12 May 2014 in Singapore

FMTV workshop website:

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

FM 2014 website:


FMTV 2014:

The first edition of FMTV was held on Monday 12 May 2014, in Singapore, in conjunction with FM 2014. About 30 participants heard  inspiring invited talks given by Wang Yi (Uppsala University, Netherlands), Samarjit Chakraborty (TU Munich, Germany) and P.S. Thiagarajan (National University of Singapore, Singapore), a presentation of an accepted scientific paper given by Andreas Stahlhofen (University of Koblenz-Landau, Germany) as well as an industrial talk given by Rafik Henia (Thales Research & Technology, France) who also presented the FMTV industrial timing challenge. A “round table” discussion on “How can Formal Methods help Industry?”, chaired by Sophie Quinton (INRIA Grenoble, France) concluded the workshop.

Two papers were accepted in this first edition of FTMV. the paper were reviewed by the international programme committee. Each paper was reviewed by 4 PC members.


Workshop Program:

9:00-9:15: Sophie Quinton, Inria Grenoble – Rhône-Alpes: Opening

9:15-10:00: Rafik Henia, Thales Research & Technology: Towards Precise Timing Modeling for Industrial System Engineering

10:00-10:30: <Conference Coffee Break Time>

10:30-11:15: Wang Yi, Uppsala University: Workload Models for System-Level Timing Analysis: Expressiveness vs. Analysis Efficiency

11:15-12:00: Samarjit Chakraborty, TU Munich: Real-Time Systems Versus Cyber-Physical Systems: Where is the Difference?

12:00-12:30: Luca Santinelli, Frédéric Boniol, Eric Noulard, Claire Pagetti and Wolfgang Puffitsch, ONERA Toulouse and TU Denmark: Integrated Development Framework for Safety-Critical Embedded Systems

12:30-14:00: <Conference Lunch Time>

14:00-14:45: P.S. Thiagarajan, National University of Singapore: Probabilistic Approximations of Hybrid Dynamics

14:45-15:15: Dieter Zöbel and Andreas Stahlhofen, Universität Koblenz-Landau: Mapping Safety Properties for Embedded Control Applications to Certifiably Correct Implementations

15:15-16:00: Rafik Henia: Presentation of the FMTV Challenge

16:00-16:30: <Conference Coffee Break Time>

16:30-17:15: Discussion of the FMTV Challenge

17:15-18:00: Panel: Timing Verification: How can Formal Methods help Industry?


Invited Speakers:

We are happy to announce that Professor Wang Yi from Uppsala University in Sweden, Professor Samarjit Chakraborty from Technische Universität München in Germany and Professor P.S. Thiagarajan from National University of Singapore have accepted our invitation to give talks at FMTV 2014.

Prof. Wang Yi talk : Workload Models for System-Level Timing Analysis: Expressiveness vs. Analysis Efficiency

Prof. Samarjit Chakraborty talk : Real-Time Systems Versus Cyber-Physical Systems: Where is the Difference?

Prof. P.S. Thiagarajan talk : Probabilistic Approximations of Hybrid Dynamics



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 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


Important Dates:

Submission deadline: 18 February, 2014 04 March 2014

Notification of acceptance: 24 March, 2014

Camera-ready papers: 11 April, 2014

FMTV’14 workshop: 12 May 2014


Submission Guidelines:

Authors may apply by sending a paper (6-15 pages) in English describing their contribution. The work does not need to be absolutely original but the paper should bring insights and contribute to the discussion of the topics of the workshop and it should not have been published as such elsewhere. Position papers, work-in-progress, surveys are also welcome. Manuscripts must be conforming to the Springer LNCS formatting guidelines: (same format as the FM 2014 papers). The submission deadline is 18th February 2014.

Authors of accepted papers shall prepare and submit a final version of their paper before 11th April 2014. Accepted papers will be distributed to the attendees in the workshop proceedings and (with the authors consent) in the workshop web page. Authors retain the full copyright of their contributions.

Submissions can be made here:


Organizing Committee:

Rafik Henia, Thales R&T, France

Julio Medina, University of Cantabria, Spain

Sophie Quinton, INRIA, France


Program Committee Chairs:

Julio Medina, University of Cantabria, Spain

Sophie Quinton, INRIA, France

Laurent Rioux, Thales R&T, France


Program Committee:

Liliana Cucu-Grosjean, LORIA, France

Miguel A. de Miguel, Uni. Politécnica de Madrid, Spain

Loïc Fejoz, Realtime-at-Work, France

Gregor Gössler, INRIA, France

Susanne Graf, VERIMAG, France

Huascar Espinoza Ortiz, Tecnalia, Spain

Simon Schliecker, Symtavision GmbH, Germany

Franck Singoff, Université de Bretagne Occidentale, France

Sara Tucci, CEA-LIST, France

Wang Yi, Uppsala University, Sweden

Nikolay Stoimenov, ETH Zurich, Switzerland



rafik.henia @

sophie.quinton @