Vis enkel innførsel

dc.contributor.authorGkolfi, Anastasia
dc.contributor.authorJohnsen, Einar Broch
dc.contributor.authorKristensen, Lars Michael
dc.contributor.authorYu, Ingrid Chieh
dc.date.accessioned2020-12-18T08:13:25Z
dc.date.available2020-12-18T08:13:25Z
dc.date.created2020-10-24T20:16:31Z
dc.date.issued2020
dc.identifier.citationGkolfi, A., Johnsen, E. B., Kristensen, L. M., & Yu, I. C. (2020). Model checking starvation for resource-aware active objects with coloured petri nets. CEUR Workshop Proceedings, 2651, 68–85.en_US
dc.identifier.issn1613-0073
dc.identifier.urihttps://hdl.handle.net/11250/2720132
dc.description.abstractDynamic resource provisioning is an important driver for pay-on-demand cloud computing. Virtualized resources open for resource awareness, such that applications may use resource management strategies to modify their deployment resource consumption at run-time. The ABS language supports the modeling of deployment decisions and resource management for active objects. An important property in this context is to ensure that the resource management does not lead to starvation of the executing objects. In previous work, we have formally translated the semantics of the ABS language into a parameterized Coloured Petri Net (CPN) model, such that any ABS program can be represented by setting the initial marking accordingly. In this paper, we characterize starvation using Computation Tree Logic (CTL), and demonstrate how CTL model checking of the CPN encoding of the ABS model, in combination with path finding, can be used to detect starvation and synthesize load balancers that guarantee starvation freedom.en_US
dc.language.isoengen_US
dc.publisherTechnical University of Aachenen_US
dc.rightsNavngivelse 4.0 Internasjonal*
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/deed.no*
dc.titleModel checking starvation for resource-aware active objects with coloured petri netsen_US
dc.typePeer revieweden_US
dc.typeJournal articleen_US
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright © 2020 for this paper by its authorsen_US
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400::Informasjons- og kommunikasjonsvitenskap: 420en_US
dc.source.pagenumber68-85en_US
dc.source.volume2651en_US
dc.source.journalCEUR Workshop Proceedingsen_US
dc.identifier.cristin1841968
cristin.ispublishedtrue
cristin.fulltextoriginal
cristin.qualitycode1


Tilhørende fil(er)

Thumbnail

Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel

Navngivelse 4.0 Internasjonal
Med mindre annet er angitt, så er denne innførselen lisensiert som Navngivelse 4.0 Internasjonal