https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Timed Actors and Their Formal Verification
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
University of Tehran, Tehran, Iran.
2023 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2023, Vol. 387, p. 1-7Conference paper, Published paper (Refereed)
Abstract [en]

In this paper we review the actor-based language, Timed Rebeca, with a focus on its formal semantics and formal verification techniques. Timed Rebeca can be used to model systems consisting of encapsulated components which communicate by asynchronous message passing. Messages are put in the message buffer of the receiver actor and can be seen as events. Components react to these messages/events and execute the corresponding message/event handler. Real-time features, like computation delay, network delay and periodic behavior, can be modeled in the language. We explain how both Floating-Time Transition System (FTTS) and common Timed Transition System (TTS) can be used as the semantics of such models and the basis for model checking. We use FTTS when we are interested in event-based properties, and it helps in state space reduction. For checking the properties based on the value of variables at certain point in time, we use the TTS semantics. The model checking toolset supports schedulability analysis, deadlock and queue-overflow check, and assertion based verification of Timed Rebeca models. TCTL model checking based on TTS is also possible but is not integrated in the tool.

Place, publisher, year, edition, pages
Open Publishing Association , 2023. Vol. 387, p. 1-7
Keywords [en]
Formal verification, Message passing, Semantics, Event-handlers, Formal Semantics, Message-passing, Modelling systems, Models checking, Real-time features, Time transition, Timed transition systems, Transition system, Verification techniques, Model checking
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-65187DOI: 10.4204/EPTCS.387.1Scopus ID: 2-s2.0-85173556560OAI: oai:DiVA.org:mdh-65187DiVA, id: diva2:1822142
Conference
Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantic, EXPRESS/SOS 2023, Antwerp, Belgium, 18 September, 2023
Available from: 2023-12-21 Created: 2023-12-21 Last updated: 2024-12-19Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Sirjani, Marjan

Search in DiVA

By author/editor
Sirjani, Marjan
By organisation
Embedded Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 50 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf