Article

Dating concurrent objects: real-time modeling and schedulability analysis

Authors:

Frank S. de Boer,

Mohammad Mahdi Jaghoori,

Einar Broch JohnsenAuthors Info & Claims

CONCUR'10: Proceedings of the 21st international conference on Concurrency theory

Pages 1 - 18

Published: 31 August 2010 Publication History

Abstract

In this paper we introduce a real-time extension of the concurrent object modeling language Creol which is based on duration statements indicating best and worst case execution times and deadlines. We show how to analyze schedulability of an abstraction of real-time concurrent objects in terms of timed automata. Further, we introduce techniques for testing the conformance between these behavioral abstractions and the executable semantics of Real-Time Creol in Real-Time Maude.

As a case study we model and analyze the schedulability of thread pools in an industrial communication platform.

References

[1]

Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183-235 (1994)

Digital Library

[2]

The ASK community systems, http://www.ask-cs.com/

[3]

de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: de Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316-330. Springer, Heidelberg (2007)

Digital Library

[4]

de Boer, F.S., Grabe, I., Jaghoori, M.M., Stam, A., Yi, W.: Modeling and analysis of thread-pools in an industrial communication platform. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 367-386. Springer, Heidelberg (2009)

Digital Library

[5]

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285(2), 187- 243 (2002)

Digital Library

[6]

Closse, E., Poize, M., Pulou, J., Sifakis, J., Venter, P., Weil, D., Yovine, S.: TAXYS: A tool for the development and verification of real-time embedded systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 391-395. Springer, Heidelberg (2001)

Digital Library

[7]

Jaghoori, M.M., de Boer, F.S., Chothia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. J. Logic and Alg. Prog. 78(5), 402-416 (2009)

[8]

Jaghoori, M.M., Longuet, D., de Boer, F.S., Chothia, T.: Schedulability and compatibility of real time asynchronous objects. In: Proc. Real Time Systems Symposium, pp. 70- 79. IEEE CS, Los Alamitos (2008)

Digital Library

[9]

Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35-58 (2007)

[10]

Kloukinas, C., Yovine, S.: Synthesis of safe, QoS extendible, application specific schedulers for heterogeneous real-time systems. In: Proc. 15th Euromicro Conference on Real-Time Systems (ECRTS 2003), pp. 287-294. IEEE Computer Society, Los Alamitos (2003)

[11]

Kyas, M., Johnsen, E.B.: A real-time extension of creol for modelling biomedical sensors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 42-60. Springer, Heidelberg (2009)

Digital Library

[12]

Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1-2), 134-152 (1997)

Digital Library

[13]

Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theoretical Computer Science 96(1), 73-155 (1992)

Digital Library

[14]

ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161-196 (2007)

Digital Library

[15]

Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 250-264. Springer, Heidelberg (2008)

Digital Library

[16]

Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1-38. Springer, Heidelberg (2008)

Digital Library

Cited By

Sirjani MKhamespanah EMechitov KAgha G(2017)A compositional approach for modeling and timing analysis of wireless sensor and actuator networksACM SIGBED Review10.1145/3166227.316623714:3(49-56)Online publication date: 22-Nov-2017
https://dl.acm.org/doi/10.1145/3166227.3166237
Nobakht Bde Boer FJaghoori MSchlatte ROssowski SLecca P(2012)Programming and deployment of active objects with application-level schedulingProceedings of the 27th Annual ACM Symposium on Applied Computing10.1145/2245276.2232086(1883-1888)Online publication date: 26-Mar-2012
https://dl.acm.org/doi/10.1145/2245276.2232086
Johnsen E(2012)Separating Cost and Capacity for Load Balancing in ABS Deployment ModelsRevised Lectures of the 11th International Symposium on Formal Methods for Components and Objects - Volume 786610.1007/978-3-642-40615-7_5(145-167)Online publication date: 24-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-40615-7_5
Show More Cited By

Dating concurrent objects: real-time modeling and schedulability analysis
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Looking for efficient implementations of concurrent objects
PaCT'11: Proceedings of the 11th international conference on Parallel computing technologies

As introduced by Taubenfeld, a contention-sensitive implementation of a concurrent object is an implementation such that the overhead introduced by locking is eliminated in the common cases, i.e., when there is no contention or when the operations ...
Linearizable concurrent objects
OOPSLA/ECOOP '88: Proceedings of the 1988 ACM SIGPLAN workshop on Object-based concurrent programming

Technological advances are making multiprocessors more readily available, but despite impressive progress at the hardware level, it is still difficult to realize these machines' potential for parallelism. In the sequential domain, “object-oriented” ...
Composing real-time concurrent objects: refinement, compatibility and schedulability
FSEN'11: Proceedings of the 4th IPM international conference on Fundamentals of Software Engineering

Concurrent objects encapsulate a processor each and communicate by asynchronous message passing; therefore, they can be composed to naturally model distributed and embedded systems. We model real-time concurrent objects using timed automata and provide ...

Comments

Information & Contributors

Information

Published In

cover image Guide Proceedings

CONCUR'10: Proceedings of the 21st international conference on Concurrency theory

August 2010

600 pages

ISBN:3642153747

Editors:
Paul Gastin
Laboratoire Spécification et Vérification, ENS de Cachan & CNRS, Cachan cedex, France
,
François Laroussinie
LIAFA, Université Paris Diderot, Paris cedex 13, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 31 August 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 11 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sirjani MKhamespanah EMechitov KAgha G(2017)A compositional approach for modeling and timing analysis of wireless sensor and actuator networksACM SIGBED Review10.1145/3166227.316623714:3(49-56)Online publication date: 22-Nov-2017
https://dl.acm.org/doi/10.1145/3166227.3166237
Nobakht Bde Boer FJaghoori MSchlatte ROssowski SLecca P(2012)Programming and deployment of active objects with application-level schedulingProceedings of the 27th Annual ACM Symposium on Applied Computing10.1145/2245276.2232086(1883-1888)Online publication date: 26-Mar-2012
https://dl.acm.org/doi/10.1145/2245276.2232086
Johnsen E(2012)Separating Cost and Capacity for Load Balancing in ABS Deployment ModelsRevised Lectures of the 11th International Symposium on Formal Methods for Components and Objects - Volume 786610.1007/978-3-642-40615-7_5(145-167)Online publication date: 24-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-40615-7_5
Johnsen ESchlatte RTapia Tarifa S(2011)A formal model of user-defined resources in resource-restricted deployment scenariosProceedings of the 2011 international conference on Formal Verification of Object-Oriented Software10.1007/978-3-642-31762-0_13(196-213)Online publication date: 5-Oct-2011
https://dl.acm.org/doi/10.1007/978-3-642-31762-0_13
Jaghoori M(2011)Composing real-time concurrent objectsProceedings of the 4th IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-29320-7_7(96-111)Online publication date: 20-Apr-2011
https://dl.acm.org/doi/10.1007/978-3-642-29320-7_7

View Options

View options

Figures

Tables

Media

View Table of Conten