Paper Info
Title
Modeling And Analyzing Adaptive User-Centric Systems In Real-Time Maude
Abstract
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 or to assist people in their specific activities. 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 component-based approach for modeling pervasive user-centric systems in a generic way and show how to instantiate the generic rules for a simple out-of-home digital advertising application and how to analyze and prove crucial properties of the system architecture through model checking and simulation. For proving time-dependent properties of systems 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 and to transform the MTL formulas into LTL formulas over the extended specification. This makes it possible to use the LTL model checker of Maude for verifying real time system properties. It is shown that component-based Real-Time Maude specifications as well as their extensions by clocks are time-robust and finite state; moreover, the above classes of formulas are tick-stabilizing if their atomic propositions are tick-stabilizing. As a consequence, model checking 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.
Year
DOI
Venue
2010
10.4204/EPTCS.36.1
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Keywords
Field
DocType
Component-based software engineering, reconfiguration, algebraic specification, term rewriting, Real-Time Maude, real-time temporal logic
Algebraic number,Model checking,Computer science,Theoretical computer science,Rewriting,Sampling (statistics),Temporal logic,Modular design,Systems architecture,User-centered design
Journal
Volume
Issue
ISSN
abs/1009.4
36
2075-2180
Citations 
PageRank 
References 
3
0.36
16
Authors
3
Name
Order
Citations
PageRank
Martin Wirsing12158267.89
Sebastian S. Bauer220011.05
Andreas Schroeder326814.36