Dating Concurrent Objects: Real-Time Modeling and Schedulability Analysis

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.