Opin vísindi

Modeling, verification, and analysis of timed actor-based models

Show simple item record

dc.contributor Háskólinn í Reykjavík
dc.contributor Reykjavik University
dc.contributor.advisor Marjan Sirjani, Ramtin Khosravi
dc.contributor.author Khamespanah, Ehsan
dc.date.accessioned 2019-06-13T10:47:38Z
dc.date.available 2019-06-13T10:47:38Z
dc.date.issued 2018-06
dc.identifier.uri https://hdl.handle.net/20.500.11815/1185
dc.description.abstract In the recent years, formal modeling and verification of realtime systems have become very important. Difficult-to-use modeling languages and inefficient analysis tools are the main obstacles to use formal methods in this domain. Timed actor model is one of the modeling paradigms which is proposed for modeling of realtime systems. It benefits from high-level object-oriented modeling facilities; however, developed analysis techniques for timed actors needs to be improved to make the actor model acceptable for the analysis of real-world applications. In this thesis, we first tackle the model checking problem of timed actors by proposing the standard semantics of timed actors in terms of fine-grained timed transition system (FGTS) and transforming it to Durational Transition Graph (DTG). This way, while the time complexity of model checking algorithms for TCTL properties, in general, is non-polynomial, we are able to check TCTL<> properties (a subset of TCTL) using model checking in polynomial time. We also improve the model checking algorithm of TCTL<> properties, obtaining time complexity of O((V lg V+E) |Φ|) instead of O(V(V+E)|Φ|) and use it for efficient model checking of timed actors. In addition, we propose a reduction technique which safely eliminates instantaneous transitions of FGTS. Using the proposed reduction technique, we provide an efficient algorithm for model checking of complete TCTL properties over the reduced transition systems. In actor-based models, the absence of shared variables and the presence of single-threaded actors along with non-preemptive execution of each message server, ensure that the execution of message servers do not interfere with each other. Based on this observation, we propose Floating Time Transition System (FTTS) as the big-step semantics of timed actors. The big-step semantics exploits actor features for relaxing the synchronization of progressof time among actors, and thereby reducing the number of states in transition systems. Considering an actor-based language, we prove there is an action-based weak bisimulation relation between FTTS and FGTS. As a result, the big-step semantics preserves event-based branching-time properties. Finally, we show how Timed Rebeca and FTTS are used as the back-end analysis technique of three different independent works to illustrate the applicability of FTTS in practice.
dc.description.sponsorship The work on this dissertation was supported by the project “Self-Adaptive Actors:SEADA” (nr. 163205-051) of the Icelandic Research Fund.
dc.language.iso en
dc.rights info:eu-repo/semantics/openAccess
dc.subject Tölvunarfræði
dc.subject Hugbúnaður
dc.subject Tímastjórnun
dc.subject Computer science
dc.subject Software development
dc.subject Time management
dc.title Modeling, verification, and analysis of timed actor-based models
dc.type info:eu-repo/semantics/doctoralThesis
dc.contributor.school Tölvunarfræðideild (HR)
dc.contributor.school School of Computer Science (RU)


Files in this item

This item appears in the following Collection(s)

Show simple item record