Finite Interval-Time Transition System for Real-Time Actors
| Autor: | Shaghayegh Tavassoli, Ehsan Khamespanah, Ramtin Khosravi |
|---|---|
| Přispěvatelé: | University of Tehran, Luís S. Barbosa, Mohammad Ali Abam, TC 1, WG 1.8 |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Bisimulation
Theoretical computer science Semantics (computer science) Modeling language Computer science Bisimulation relation Interval-Time Transition System 020207 software engineering 0102 computer and information sciences 02 engineering and technology Interval (mathematics) Formal methods 01 natural sciences Timed Rebeca 010201 computation theory & mathematics Transition system 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] Actor model Formal verification |
| Zdroj: | Lecture Notes in Computer Science 3rd International Conference on Topics in Theoretical Computer Science (TTCS) 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⟩ Topics in Theoretical Computer Science ISBN: 9783030578510 TTCS |
| DOI: | 10.1007/978-3-030-57852-7_7⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|