Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Distributability of Mobile Ambients
102
0
0.0
(
0
)
Added by
EPTCS
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Kirstin Peters
Ask ChatGPT about the research
No Arabic abstract
Modern society is dependent on distributed software systems and to verify them different modelling languages such as mobile ambients were developed. To analyse the quality of mobile ambients as a good foundational model for distributed computation, we analyse the level of synchronisation between distributed components that they can express. Therefore, we rely on earlier established synchronisation patterns. It turns out that mobile ambients are not fully distributed, because they can express enough synchronisation to express a synchronisation pattern called M. However, they can express strictly less synchronisation than the standard pi-calculus. For this reason, we can show that there is no good and distributability-preserving encoding from the standard pi-calculus into mobile ambients and also no such encoding from mobile ambients into the join-calculus, i.e., the expressive power of mobile ambients is in between these languages. Finally, we discuss how these results can be used to obtain a fully distributed variant of mobile ambients.
rate research
Read More
We formalise a general concept of distributed systems as sequential components interacting asynchronously. We define a corresponding class of Petri nets, called LSGA nets, and precisely characterise those system specifications which can be implemented as LSGA nets up to branching ST-bisimilarity with explicit divergence.
We propose a framework to build formal developments for robot networks using the COQ proof assistant, to state and to prove formally various properties. We focus in this paper on impossibility proofs, as it is natural to take advantage of the COQ higher order calculus to reason about algorithms as abstract objects. We present in particular formal proofs of two impossibility results forconvergence of oblivious mobile robots if respectively more than one half and more than one third of the robots exhibit Byzantine failures, starting from the original theorems by Bouzid et al.. Thanks to our formalization, the corresponding COQ developments are quite compact. To our knowledge, these are the first certified (in the sense of formally proved) impossibility results for robot networks.
Cyber-Physical Systems~(CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, the spatial and temporal requirements play an essential role for their correct and safe execution. Furthermore, the local interactions among the system components result in global spatio-temporal emergent behaviors often impossible to predict at the design time. In this work, we pursue a complementary approach by introducing STREL a novel spatio-temporal logic that enables the specification of spatio-temporal requirements and their monitoring over the execution of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic with two novel spatial operators reach and escape from which is possible to derive other spatial modalities such as everywhere, somewhere and surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbours, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimisation. We prove that, for a subclass of models, all the spatial properties expressed with reach and escape, using euclidean distance, satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for STREL and, to demonstrate the feasibility of our approach, we show its application using the monitoring of a simulated mobile ad-hoc sensor network as running example.
BioScape is a concurrent language motivated by the biological landscapes found at the interface of biology and biomaterials. It has been motivated by the need to model antibacterial surfaces, biofilm formation, and the effect of DNAse in treating and preventing biofilm infections. As its predecessor, SPiM, BioScape has a sequential semantics based on Gillespies algorithm, and its implementation does not scale beyond 1000 agents. However, in order to model larger and more realistic systems, a semantics that may take advantage of the new multi-core and GPU architectures is needed. This motivates the introduction of parallel semantics, which is the contribution of this paper: Parallel BioScape, an extension with fully parallel semantics.
Mobile web browsing has recently surpassed desktop browsing both in term of popularity and traffic. Following its desktop counterpart, the mobile browsers ecosystem has been growing from few browsers (Chrome, Firefox, and Safari) to a plethora of browsers, each with unique characteristics (battery friendly, privacy preserving, lightweight, etc.). In this paper, we introduce a browser benchmarking pipeline for Android browsers encompassing automation, in-depth experimentation, and result analysis. We tested 15 Android browsers, using Cappuccino a novel testing suite we built for third party Android applications. We perform a battery-centric analysis of such browsers and show that: 1) popular browsers tend also to consume the most, 2) adblocking produces significant battery savings (between 20 and 40% depending on the browser), and 3) dark mode offers an extra 10% battery savings on AMOLED screens. We exploit this observation to build AttentionDim, a screen dimming mechanism driven by browser events. Via integration with the Brave browser and 10 volunteers, we show potential battery savings up to 30%, on both devices with AMOLED and LCD screens.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
