Finite Interval-Time Transition System for Real-Time Actors - Topics in Theoretical Computer Science Access content directly
Conference Papers Year : 2020

Finite Interval-Time Transition System for Real-Time Actors

Ramtin Khosravi
  • Function : Author
  • PersonId : 999434


Real-time computer systems are software or hardware systems which have to perform their tasks according to a time schedule. Formal verification is a widely used technique to make sure if a real-time system has correct time behavior. Using formal methods requires providing support for non-deterministic specification for time constraints which is realized by time intervals. Timed-Rebeca is an actor-based modeling language which is equipped with a verification tool. The values of timing features in this language are positive integer numbers and zero (discrete values). In this paper, Timed-Rebeca is extended to support modeling timed actor systems with time intervals. The semantics of this extension is defined in terms of Interval-Time Transition System (ITTS) which is developed based on the standard semantics of Timed-Rebeca. In ITTS, instead of integer values, time intervals are associated with system states and the notion of shift equivalence relation in ITTS is used to make the transition system finite. As there is a bisimulation relation between the states of ITTS and finite ITTS, it can be used for verification against branching-time properties.
Fichier principal
Vignette du fichier
495613_1_En_7_Chapter.pdf (505.82 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03165386 , version 1 (10-03-2021)





Shaghayegh Tavassoli, Ramtin Khosravi, Ehsan Khamespanah. Finite Interval-Time Transition System for Real-Time Actors. 3rd International Conference on Topics in Theoretical Computer Science (TTCS), Jul 2020, Tehran, Iran. pp.85-100, ⟨10.1007/978-3-030-57852-7_7⟩. ⟨hal-03165386⟩
37 View
17 Download



Gmail Facebook X LinkedIn More