Skip to Main content Skip to Navigation
Conference papers

Finite Interval-Time Transition System for Real-Time Actors

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03165386
Contributor : Hal Ifip <>
Submitted on : Wednesday, March 10, 2021 - 4:05:24 PM
Last modification on : Wednesday, March 10, 2021 - 4:07:11 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

4