In today's technology-assisted society, social interactions may be expressed through a variety of techno-communication channels, including online social networks, email and mobile phones (calls, text messages). Consequently, a clear grasp of human behavior through the diverse communication media is considered a key factor in understanding the formation of the today's information society. So far, all previous research on user communication behavior has focused on a sole communication activity. In this paper we move forward another step on this research path by performing a multidimensional study of human sociality as an expression of the use of mobile phones. The paper focuses on user temporal communication behavior in the interplay between the two complementary communication media, text messages and phone calls, that represent the bi-dimensional scenario of analysis. Our study provides a theoretical framework for analyzing multidimensional bursts as the most general burst category, that includes one-dimensional bursts as the simplest case, and offers empirical evidence of their nature by following the combined phone call/text message communication patterns of approximately one million people over three-month period. This quantitative approach enables the design of a generative model rooted in the three most significant features of the multidimensional burst - the number of dimensions, prevalence and interleaving degree - able to reproduce the main media usage attitude. The other findings of the paper include a novel multidimensional burst detection algorithm and an insight analysis of the human media selection process.

Engineering distributed self-adaptive systems is challenging due to multiple interacting components, some of which monitor and possibly modify the behavior of managed components that operate in highly dynamic settings. Formalizing such systems having a decentralized adaptation control has been recognized as a hard task. In this article, we introduce a formal framework based on Symmetric Nets (a well-established subclass of Colored Petri nets) for modeling and analyzing distributed self-adaptive discrete-event systems. Even though Petri Nets represent a sound and expressive formal model of concurrency and distribution, they cannot specify in a natural way structural changes enacted by adaptation procedures. We overcome this limitation by means of a two-layer modeling approach that enables clear separation of concerns and allows multiple decentralized adaptation procedures to be specified, validated, and verified against formal requirements. Validation and verification techniques are supported by powerful off-the-shelf tools tailored to Symmetric Nets. A self-healing manufacturing system case study is used to show applicability, advantages, and shortcomings of the approach. In particular, complexity issues are thoroughly discussed and mitigated by adopting complementary approaches based on interleaving reduction and behavioral symmetries exploitation.

Twenty-eight children with beta-thalassaemia major aged between 11 and 48 months were given intensive transfusions. Serum iron, transferrin saturation, serum ferritin, non-transferrin iron, and subcutaneous desferrioxamine-induced urinary iron excretion were measured. The results showed that even children with a limited number of transfusions had severe iron overload as indicated, in particular, by the raised serum ferritin levels and the high excretion rates after subcutaneous infusion of desferrioxamine. The desferrioxamine test was useful, even in very young children, in assessing response to chelation therapy thus enabling such treatment to be started early to prevent harm from iron overload.

The recent extensive availability of "big data" platforms calls for a widespread adoption by the formal verification community. Cloud computing platforms represent a great opportunity to run massively parallel jobs, yet classical formal verification tools/techniques must undergo a deep technological transformation in order to exploit the new available architectures. This has raised an increasing interest in deploying verification techniques on parallel/distributed frameworks. In this paper we introduce a framework to ease the adoption of a distributed approach to verification of Computation Tree Logic (CTL) formulas on very large state spaces. The approach exploits/integrates a recently developed, parametric state-space builder. The whole framework adopts M AP R EDUCE as core computational model, and can be tailored to different modelling formalisms. The outcomes of several tests performed on (Petri-nets based) benchmark specifications are presented, thus showing the convenience of the proposed approach.