English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Pervasive user-centric applications are systems which are meant to sense thepresence, mood, and intentions of users in order to optimize user comfort andperformance. Building such applications requires not only state-of-the arttechniques from artificial intelligence but also sound software engineeringmethods for facilitating modular design, runtime adaptation and verification ofcritical system requirements.  In this paper we focus on high-level design and analysis, and use thealgebraic rewriting language Real-Time Maude for specifying applications in areal-time setting. We propose a generic component-based approach for modelingpervasive user-centric systems and we show how to analyze and prove crucialproperties of the system architecture through model checking and simulation.For proving time-dependent properties we use Metric Temporal Logic (MTL) andpresent analysis algorithms for model checking two subclasses of MTL formulas:time-bounded response and time-bounded safety MTL formulas. The underlying ideais to extend the Real-Time Maude model with suitable clocks, to transform theMTL formulas into LTL formulas over the extended specification, and then to usethe LTL model checker of Maude. It is shown that these analyses are sound andcomplete for maximal time sampling. The approach is illustrated by a simpleadaptive advertising scenario in which an adaptive advertisement display canreact to actions of the users in front of the display.

Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude