Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude
Pervasive user-centric applications are systems which are meant to sense the presence, mood, and intentions of users in order to optimize user comfort and performance. Building such applications requires not only state-of-the art techniques from artificial intelligence but also sound software engine...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2010-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1009.4259v1 |
| _version_ | 1818116387301752832 |
|---|---|
| author | Andreas Schroeder Sebastian S. Bauer Martin Wirsing |
| author_facet | Andreas Schroeder Sebastian S. Bauer Martin Wirsing |
| author_sort | Andreas Schroeder |
| collection | DOAJ |
| description | Pervasive user-centric applications are systems which are meant to sense the presence, mood, and intentions of users in order to optimize user comfort and performance. Building such applications requires not only state-of-the art techniques from artificial intelligence but also sound software engineering methods for facilitating modular design, runtime adaptation and verification of critical system requirements. In this paper we focus on high-level design and analysis, and use the algebraic rewriting language Real-Time Maude for specifying applications in a real-time setting. We propose a generic component-based approach for modeling pervasive user-centric systems and we show how to analyze and prove crucial properties of the system architecture through model checking and simulation. For proving time-dependent properties we use Metric Temporal Logic (MTL) and present analysis algorithms for model checking two subclasses of MTL formulas: time-bounded response and time-bounded safety MTL formulas. The underlying idea is to extend the Real-Time Maude model with suitable clocks, to transform the MTL formulas into LTL formulas over the extended specification, and then to use the LTL model checker of Maude. It is shown that these analyses are sound and complete for maximal time sampling. The approach is illustrated by a simple adaptive advertising scenario in which an adaptive advertisement display can react to actions of the users in front of the display. |
| first_indexed | 2024-12-11T04:21:42Z |
| format | Article |
| id | doaj.art-cd07704308804a03b3cfe37c8c7e0aef |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T04:21:42Z |
| publishDate | 2010-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-cd07704308804a03b3cfe37c8c7e0aef2022-12-22T01:21:06ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-09-0136Proc. RTRTS 201012510.4204/EPTCS.36.1Modeling and Analyzing Adaptive User-Centric Systems in Real-Time MaudeAndreas SchroederSebastian S. BauerMartin WirsingPervasive user-centric applications are systems which are meant to sense the presence, mood, and intentions of users in order to optimize user comfort and performance. Building such applications requires not only state-of-the art techniques from artificial intelligence but also sound software engineering methods for facilitating modular design, runtime adaptation and verification of critical system requirements. In this paper we focus on high-level design and analysis, and use the algebraic rewriting language Real-Time Maude for specifying applications in a real-time setting. We propose a generic component-based approach for modeling pervasive user-centric systems and we show how to analyze and prove crucial properties of the system architecture through model checking and simulation. For proving time-dependent properties we use Metric Temporal Logic (MTL) and present analysis algorithms for model checking two subclasses of MTL formulas: time-bounded response and time-bounded safety MTL formulas. The underlying idea is to extend the Real-Time Maude model with suitable clocks, to transform the MTL formulas into LTL formulas over the extended specification, and then to use the LTL model checker of Maude. It is shown that these analyses are sound and complete for maximal time sampling. The approach is illustrated by a simple adaptive advertising scenario in which an adaptive advertisement display can react to actions of the users in front of the display.http://arxiv.org/pdf/1009.4259v1 |
| spellingShingle | Andreas Schroeder Sebastian S. Bauer Martin Wirsing Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude Electronic Proceedings in Theoretical Computer Science |
| title | Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude |
| title_full | Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude |
| title_fullStr | Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude |
| title_full_unstemmed | Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude |
| title_short | Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude |
| title_sort | modeling and analyzing adaptive user centric systems in real time maude |
| url | http://arxiv.org/pdf/1009.4259v1 |
| work_keys_str_mv | AT andreasschroeder modelingandanalyzingadaptiveusercentricsystemsinrealtimemaude AT sebastiansbauer modelingandanalyzingadaptiveusercentricsystemsinrealtimemaude AT martinwirsing modelingandanalyzingadaptiveusercentricsystemsinrealtimemaude |