More Web Proxy on the site http://driver.im/

Article

From the Specification to the Scheduling of Time-Dependent Systems

Authors:

Christophe Lohr,

Jean-Pierre CourtiatAuthors Info & Claims

FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2

Pages 129 - 146

Published: 09 September 2002 Publication History

Abstract

This paper introduces and formalizes a new variant of Timed Automata, called Time Labeled Scheduling Automata. A Time Labeled Scheduling Automaton is a single clock implementation model expressing globally the time constraints that a system has to meet. An algorithm is presented to show how a Time Labeled Scheduling Automaton can be synthesized from a minimal reachability graph derived from a high-level specification expressing the composition of different time constraints. It is shown how the reachability graph may be corrected before synthesizing the Time Labeled Scheduling Automaton to remove all its potentially inconsistent behaviors. Current applications of the model are the scheduling of interactive multimedia documents and a simple illustration is given in this area.

References

[1]

K. Altisen, G. Gossler, and J. Sifakis. A methodology for the construction of scheduled systems. In FTRTFT 2000 , volume 1926 of Lecture Notes in Computer Science , pages 106-120, Pune, India, September 2000.

[2]

R. Alur, C. Courcoubetis, and N. Halbwachs. Minimization of timed transition systems. In CONCUR'92 , volume 630 of Lecture Notes in Computer Science . Springer Verlag, 1992.

[3]

R. Alur and D. Dill. The theory of timed automata. In REX Workshop "Real-Time: Theory in Practice ", volume 600 of Lecture Notes in Computer Science . Springer Verlag, 1991.

[4]

R. Alur, L. Fix, and T.A. Heizinger. Event-clock automata : A determinizable class of timed automata. In 6th Annual Conference on Computeraided Verification , Lecture Notes in Computer Science 818, pages 1-13. Springer Verlag, 1994.

[5]

E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems , pages 1-20, 1994.

[6]

B. Berthomieu and M. Diaz. Modeling and verification of time-dependent systems using time Petri nets. In IEEE Transactions on Software Engineering , volume 17. no. 3, 1991.

[7]

J.P. Courtiat and R.C. R. de Oliveira. A reachability analysis of RT-Lotos specifications. In 8th International Conference on Formal Description Techniques , Montreal, Canada, October 1995. Chapman&Hall.

[8]

J.P. Courtiat, C.A.S. Santos, C. Lohr, and B. Outtaj. Experience with RT-Lotos, a temporal extension of the Lotos formal description technique. Computer Communications , 23:1104-1123, 2000.

[9]

H. Dierks. Synthesising controllers from real-time specifications. In Tenth International Symposium on System Synthesis , pages 126-133. IEEE Computer Society, September 1997.

[10]

I. Kang and I. Lee. An efficient state space generation for analysis of real-time systems. In International Symposium on Software Testing and Analysis , pages 4-13, 1996.

[11]

X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In REX Workshop "Real-Time: Theory in Practice ", volume 600 of Lecture Notes in Computer Science . Springer Verlag, 1991.

[12]

A. Pnueli, E. Asarin, O. Maler, and J. Sifakis. Controller synthesis for timed automata. In System Structure and Control . Elsevier Science, 1998.

[13]

P.N.M. Sampaio and J.P. Courtiat. A formal approach for the presentation of interactive multimedia documents. In ACM Multimedia'2000 , pages 435-438, Los Angeles, USA, October 2000.

[14]

P.N.M. Sampaio and J.P. Courtiat. Scheduling and presenting interactive multimedia documents. In International Conference on Multimedia and Exposition'2001 , pages 1227-1227, Tokyo, Japan, August 2001.

[15]

P.N.M. Sampaio, C. Lohr, and J.P. Courtiat. An integrated environment for the presentation of consistent SMIL 2.0 documents. In ACM Symposium on Document Engineering , Atlanta, Georgia, USA, November 2001.

[16]

C.A.S. Santos, P.N.M. Sampaio, and J.P. Courtiat. Revisiting the concept of hypermedia document consistency. In ACM Multimedia'99 , Orlando, USA, November 1999.

[17]

P. Sénac, M. Diaz, A. Leger, and P. de Saqui-Sannes. Modelling logical and temporal synchronization in hypermedia systems. In IEEE Journal on Selected Areas in Communications , volume 14(1), pages 84-103, January 1996.

[18]

M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In CAV'93 , volume 697 of Lecture Notes in Computer Science . Springer Verlag, 1993.

Cited By

Picinin Júnior DFarines JSantos CWillrich RLima J(2011)An MDE approach for Modeling and Verification of Interactive Multimedia DocumentsProceedings of the 17th Brazilian Symposium on Multimedia and the Web on Brazilian Symposium on Multimedia and the Web - Volume 110.5555/3021508.3021521(89-96)Online publication date: 3-Oct-2011
https://dl.acm.org/doi/10.5555/3021508.3021521
Sampaio PPeralta LCourtiat J(2007)Designing consistent multimedia documentsProceedings of the 5th international conference on Formal modeling and analysis of timed systems10.5555/1779879.1779900(290-303)Online publication date: 3-Oct-2007
https://dl.acm.org/doi/10.5555/1779879.1779900
Apvrille LCourtiat JLohr Cde Saqui-Sannes P(2004)TURTLEIEEE Transactions on Software Engineering10.1109/TSE.2004.3430:7(473-487)Online publication date: 1-Jul-2004
https://dl.acm.org/doi/10.1109/TSE.2004.34

Recommendations

From nonpreemptive to preemptive scheduling: from single-processor to multi-processor?
SAC '11: Proceedings of the 2011 ACM Symposium on Applied Computing

The use of automata for specifying patterns of task generation has broaden the perspective of schedulability analysis; scheduling has moved from periodic or rate-monotonic to aperiodic and non-uniform tasks. The question of schedulability in this ...
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems

Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., ...
Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique

This paper is devoted to the presentation of the RT-LOTOS formal description technique, which is a formalism suited for applications where concurrency, complex synchronization patterns, asynchronous interactions and timing constraints have to be dealt ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2

September 2002

451 pages

ISBN:3540441654

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 09 September 2002

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Picinin Júnior DFarines JSantos CWillrich RLima J(2011)An MDE approach for Modeling and Verification of Interactive Multimedia DocumentsProceedings of the 17th Brazilian Symposium on Multimedia and the Web on Brazilian Symposium on Multimedia and the Web - Volume 110.5555/3021508.3021521(89-96)Online publication date: 3-Oct-2011
https://dl.acm.org/doi/10.5555/3021508.3021521
Sampaio PPeralta LCourtiat J(2007)Designing consistent multimedia documentsProceedings of the 5th international conference on Formal modeling and analysis of timed systems10.5555/1779879.1779900(290-303)Online publication date: 3-Oct-2007
https://dl.acm.org/doi/10.5555/1779879.1779900
Apvrille LCourtiat JLohr Cde Saqui-Sannes P(2004)TURTLEIEEE Transactions on Software Engineering10.1109/TSE.2004.3430:7(473-487)Online publication date: 1-Jul-2004
https://dl.acm.org/doi/10.1109/TSE.2004.34

View Options

View options

Media

Figures

Other

Tables

View Table of Contents