Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Call For Participation, FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS'2003)
[go: Go Back, main page]

First International Workshop on

Formal Modeling and Analysis of Timed Systems

FORMATS 2003

September 6-7 2003, Marseille, France

(co-located with the International Conference on Concurrency Theory, CONCUR, inscription on CONCUR inscription page , see at bottom)

OBJECTIVES


In the past timing aspects of systems from a variety of computer science domains have been treated independently in separate scientific disciplines: People who are interested in semantics, verification or performance analysis are working on models such as timed automata, timed Petri nets or max-plus algebra. Electrical engineers have to consider propagation delays in their circuits and designers of embedded controllers have to take into account the time it takes for the controller to compute its reaction after sampling the environment.

While indeed the timing related questions in these separate disciplines have their particularities (e.g. worst case analysis vs. average case optimisation), there is a growing awareness of the difficult problems common to all of them, suggesting the interdisciplinary study of Timed Systems: The unifying theme underlying all these apparently different domains is that they treat systems whose behavior depends upon combinations of logical and temporal constraints, i.e. constraints on the distance between the occurrences of two events.

FORMATS is aimed to be a major annual event dedicated to the study of Timed Systems, uniting three independently started workshop series related to the topic: MTCS (held as satellite event of CONCUR'00-02), RT-TOOLS(held as satellite event of CONCUR'01 and FLoC'02) and TPTS (at ETAPS'02), with a total in 2002 of around 100 individual participants. In 2003, it will be held in link with CONCUR'2003 (International Conference on Concurrency theory), thus with the potential of attracting participants from neighbouring disciplines.

PROGRAMME (preliminary)


Saturday 6/9/2003

9h00
Opening

9h15
Evgeny Asarin (invited speaker)

10h15 break


Model Checking I

10h30 Towards Refining Partitioning for Checking Reachability in Timed Automata
A. Pó\x{0142}rola, W. Penczek, M. Szreter
11h00
Checking ACTLS properties of Discrete Timed Automata via Bounded Model Checking
B. Wozna and A. Zbrzezny
11h30
Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently
Zhao J., Li X., Zheng T., Zheng G.
12h00
Adding Symmetry Reduction to UppAal
M. Hendriks, G. Behrmann, K.G. Larsen, P. Niebert, F.Vaandrager
12h30-14h00
lunch break


Timed and probabilistic optimization

14h00
Status and Development of the TIMES Tool  T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson and W. Yi
14h30 Optimization of Timed Automata Models Using Mixed-Integer Programming  O. Stursberg, S. Panek
15h00 Discrete-time rewards model-checked S.Andova, H.Hermanns, J.-P. Katoen
15h30
Performance Analysis of Probabilistic Timed Automata using Digital Clocks M. Kwiatkowska, G. Norman, D. Parker, J. Sproston
16h00
break


Theory

16h30
An interval-based algebra for restricted event detection J. Carlson and B. Lisper
17h00
PARS: A Process Algebra with Resources and Schedulers   M. Mousavi, M. Reniers, T. Basten, M. Chaudron
17h30
Formal Semantics of Hybrid Chi R.R.H. Schiffelers, D.A. van Beek,
K.L. Man, M.A. Reniers and J.E. Rooda
18h00 End day 1

20h00
Workshop Dinner


Sunday 7/9/2003

9h15 Reinhard Wilhelm (invited speaker)

10h15 break


Theory

10h30 A nonarchimedian discretization for timed languages C. Dima
11h00
Folk theorems on the determinization and minimization of timed automata S. Tripakis

Applications

11h30 Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking
F. Vaandrager and B. Gebremichael
12h00
On Timing Analysis of Combinational Circuits R.B. Salah, M. Bozga and O. Maler
12h30
Analysis of Real Time Operating System Based Applications L. Waszniowski, Z. Hanzalek
13h00-14h30 lunch break

14h30

Paul Petterson (invited speaker)
15h30 break




Petri nets and Partial Order Semantics
16h00 Using Zone Graph Method for Computing the State Space of a Time Petri Net G. Gardey, O.H. Roux, O.F. Roux
16h30
Causal Time Calculus F.Pommereau
17h00
ELSE: A new symbolic state generator for timed automata S. Zennou and M. Yguel and P. Niebert
17h30
closing



STEERING COMMITTEE

Rajeev Alur (USA) Flavio Corradini (Italy) Kim G. Larsen (Denmark)
Oded Maler (France) Walter Vogler (Germany) Wang Yi(Sweden)


PROGRAM COMMITTEE

Rajeev Alur (USA)
Jos Baeten (Netherlands)

Alan Burns (United Kingdom)
Flavio Corradini (Italy) Jordi Cortadella (Spain)
Pedro D'Argenio (Argentina) Thomas A. Henzinger(USA) Joost-Pieter Katoen (Netherlands)
Marta Kwiatkowska (United Kingdom) François Laroussinie (France) Kim G. Larsen (Denmark, co-chair)
Claude LePape (France) Oded Maler  (France) Peter Niebert (France, co-chair)
Ernst-Rüdiger Olderog (Germany) Paritosh K. Pandya  (India) Wojciech Penczek (Poland)
Olaf Stursberg (Germany) P.S. Thiagarajan (Singapore) Stavros Tripakis (France)
Frits Vaandrager (Netherlands) Walter Vogler (Germany) Wang Yi (Sweden)

INVITED SPEAKERS

Eugene Asarin (VERIMAG, Grenoble, France)
Paul Petterssen (Univ. Uppsala, Sweden)
Reinhard Wilhelm (Unversity of Saarbrücken, Germany)

VENUE AND INSCRIPTION

FORMATS 2003 is held as a workshop of (and directly succeeding) CONCUR'2003, which is held september 3-5. Please visit also the CONCUR'2003 web site for more information about organisation and other reasons to come! Inscription to FORMATS is via the CONCUR inscription page. Note that you get a reduction if you sign in for both CONCUR and FORMATS.

CONTACT

For any question concerning the workshop, please contact Peter Niebert (co-chair)

SPONSOR

FORMATS'2003 is strongly supported by the European project IST-2001-35304 AMETIST (Advanced MEthods in TImed SysTems).