The rate-monotonic algorithm is arguably one of the most popular algorithms for scheduling systems of periodic real-time tasks. The rate-monotonic scheduling of systems of periodic tasks on uniform multiprocessor platforms is considered here. A simple, sufficient test is presented for determining whether a given periodic task system will be successfully scheduled by this algorithm upon a particular uniform multiprocessor platform --- this test generalizes earlier results concerning rate-monotonic scheduling upon identical multiprocessor platforms.

We consider the problem of model-checking a parametric extension of the logic TCTL over timed automata and establish its decidability. We show that the notion of durations between regions defined by a timed automaton is expressible in the arithmetic of Presburger (when the time domain is discrete) or in the theory of the reals (when the time domain is dense). When this notion of duration is formalized in those theories, we show that the parametric model-checking problem for the logic TCTL can easily be solved.

In this paper we define a property for multi-party protocols called exclusion-freeness. In multi-party protocols respecting the strongest definition of this property, participants are sure that they will not be excluded from a protocol's execution and, consequently, they do not have to trust each other any more. We study this property on a well-known multi-party fair exchange protocol with an online trusted third party and we point out two attacks on this protocol breaking the fairness property and implying excluded participants. Finally, we propose a new multi-party fair exchange protocol with an online trusted third party respecting the strong exclusion-freeness property.

In this paper we report on the verification of two contract signing protocols. Our verification method is based on the idea of modeling those protocols as games, and reasoning about their properties as strategies for players. We use the formal model of alternating transition systems to represent the protocols and alternating-time temporal logic to specify properties. The paper focuses on the verification of abuse-freeness, relates this property to the balance property, previously studied using two other formalisms, shows some ambugities in the definition of abuse-freeness and proposes a new, stronger definition. Formal methods are not only useful here to verify automatically the protocols but also to better understand their requirements (balance and abuse-freeness are quite complicated and subtle properties).

With the phenomenal growth of the Internet and open networks in general, security services, such as non-repudiation, become crucial to many applications. Non-repudiation services must ensure that when Alice sends some information to Bob over a network, neither Alice nor Bob can deny having participated in a part or the whole of this communication. Therefore a non-repudiation protocol has to generate non-repudiation of origin evidences intended to Bob, and non-repudiation of receipt evidences destined to Alice. In this paper, we clearly define the properties a non-repudiation protocol must respect, and give a survey of the most important non-repudiation protocols without and with trusted third party (TTP). For the later ones we discuss the evolution of the TTP's involvement and, between others, describe the most recent protocol using a transparent TTP. We also discuss some ad-hoc problems related to the management of non-repudiation evidences and briefly overview several efforts on formal verification ofnon-repudiation protocols.

The need for dynamic loading of power components in the deregulated electricity market demands for reliable assessment models that should be able to predict the thermal behaviour when the load exceeds the nameplate value. When assessing network load capability, the hot spot temperature of the components is known to be the most critical factor. The knowledge of the evolution of the hot spot temperature during overload conditions is essential to evaluate the loss of insulation life and to evaluate the consequent risks of both technical and economical nature. This paper discusses an innovative grey-box architecture for integrating physical knowledge modelling (a.k.a. white-box) with machine learning techniques (a.k.a. black-box). In particular, we focus on the problem of forecasting the hot spot temperature of a mineral-oil-immersed transformer. We perform a set of experiments and we compare the predictions obtained by the grey-,white-, and black-box approaches.