The optimal resources allocation to tasks was the primary objective of the research dealing with scheduling problems. These problems are characterized by their complexity, known as NP-hard in most cases. Currently with the evolution of technology, classical methods are inadequate because they degrade system performance (inflexibility, inefficient resources using policy, etc.). In the context of parallel and distributed systems, several computing units process multitasking applications in concurrent way. Main goal of such process is to schedule tasks and map them on the appropriate machines to achieve the optimal overall system performance (Minimize the Make-span and balance the load among the machines). In this paper we present a Time Petri Net (TPN) based approach to solve the scheduling problem by mapping each entity (tasks, resources and constraints) to correspondent one in the TPN. In this case, the scheduling problem can be reduced to finding an optimal sequence of transitions leading from an initial marking to a final one. Our approach improves the classical mapping algorithms by introducing a control over resources allocation and by taking into consideration the resource balancing aspect leading to an acceptable state of the system. The approach is applied to a specific class of problems where the machines are parallel and identical. This class is analyzed by using the TiNA (Time Net Analyzer) tool software developed in the LAAS laboratory (Toulouse, France).

The main objective of this paper is to secure a cross-layer, energy efficient MAC protocol (CL-MAC) dedicated to delay sensitive wireless sensor networks (WSN) for detecting and avoiding wormhole attack. CL-MAC protocol is the result of our previous research works for which the security aspects have not been taken into consideration during its design stage. To formally prove the importance of the proposed scheme, we provide a theoretical study based on Time Petri Net to analyse some important properties related to the devastating effect of the wormhole attack and its countermeasure on the CL-MAC operations. Also, we perform an experimental evaluation through the simulation using realistic scenarios in order to show the performance of the proposal in terms of energy saving, packets loss ratio and latency. The obtained results indicate the usefulness of the formal study provided in this work when applied in security context and confirm clearly a good performance of the proposed scheme against wormhole attack.

This paper is a contribution for development of a high level of security for the Programmer Logic Controller (PLC). Many industrial adopt the redundant PLC architecture (or Standby PLC) designed to replace the failed (out of order) PLC without stopping associated automated equipments. We propose a formal method to choose a Standby PLC based on probability study, by comparing normal functioning to misbehavior one leading to residue generation process. Any generated difference reveals a presence of anomaly. The proposed method begins by listing all PLC components failures leading to their stopping according to failures criticalities. Two models; functional and dysfunctional are obtained by using formal specifications. Probability’s calculus of dysfunction of each Standby PLC is obtained by the sum of the probabilities of dysfunction of its critical components. These probabilities are allocated each transition which leads to the dysfunction in the dysfunctional model. The dysfunctional model is obtained by using the FMECA method (Failure Modes, Effects and Criticality Analysis). We shall see that this global vision of functioning of the whole PLC leads to a higher level of security where the chosen Standby PLC works continuously.

Hybrid dynamic systems are analyzed through linear hybrid automaton. In this paper, we propose a mapping algorithm to deal with a new Continuous elementary HPN. The method shown enables us to analyze some system properties using a linear hybrid automaton generated by a mapping process. The application involves a water system of three tanks, which is analyzed by a PHAVer (Polyhedral Hybrid Automaton Verifier) software tool. Its effectiveness is illustrated by numerical simulation results.