Timed Actors and Their Formal Verification
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
2023-12-212023-12-212024-12-19Bibliographically approved