Abstract: Formal modelling techniques can be used for analysis of wireless sensor networks (WSNs). High
level Petri nets (HLP-nets) that is an extension of Petri nets is a powerful modelling technique.
This paper presents a HLP-nets based approach for formal modelling and analysis of WSNs.
The proposed model uses the hierarchical modelling capability of HLP-nets. The presented
model includes different levels of abstraction. The proposed HLP-net model is quite general and
generic to present a large class of WSN behaviour. The presented model globally represents the
behaviour of all the WSN components (nodes and bases station). The designer can choose the
specific level of abstraction.
The interfacing of the HLP-net models representing the node operations is made through the
model semantics and the fusion places. No additional efforts must be done to synchronise all
the models.
Add to the simulation possibility, formal verification of the network properties is also enabled
based on the proposed HLP-net model.
Abstract: We present an approach for formal modelling and analysis of sensor network based on coloured Petri nets (CP-nets). Presented model consider various level of abstraction. It takes into account several aspects: the protocols, the application, an abstracted energy consumption model of the hardware and a view of the environment as observed by each node. Simulation may be used to validate the behaviour of the studied network. A major difference distinguishing the proposed method of all the existing simulators is that the CP-net model allows formal verification of the network properties. The proposed approach is illustrated with a simple example of a sensor network dedicated to forest fire detection. We show also what properties could be formally verified based on the proposed CP-net.
Abstract: Wireless sensor network consists of a large number of low-power, short-lived, unreliable sensors. One fundamental issue in this kind of networks is the textbf{coverage} problem, that reflects how well the target area is monitored by sensors. According to the coverage concept, many works have introduced nodes-scheduling methods to increase the system lifetime, as well as to maintain sufficient coverage and reliability. Node-scheduling allows to turn off redundant sensors. In this paper, we propose a node-scheduling algorithm, that reduces system overall energy consumption, therefore increasing system lifetime, by turning off redundant nodes. The proposed scheduling method is based on one-hop remaining energy neighbouring knowledge. This algorithm gives an optimal node-schedul that maintains the original sensing coverage after turning off redundant nodes.
Abstract: Recent advances in wireless sensor networks have led to many new protocols specifically designed for sensor networks where energy awareness is an essential consideration. Attention has been mostly directed towards routing protocols. These protocols generally implement a view embracing a local energy reserve. This paper presents an algorithm for determining optimal paths connecting sensor nodes to the sink. These optimal paths contribute to minimizing intermediate hops and consider a global energy reserve. Most of these sensor networks will require application specific functionalities and performance requirements because of the wide range of their applications. Modelling sensor network behaviour before implementation and deployment is therefore crucial to programming efficiently the network application and to validating all its protocols. Existing works suffer from the problem of insufficient formal models for sensor network validations. Such models enable formal verification of all sensor network properties prior to deployment. This paper will also present a formal model representing sensor network behaviour.
Abstract: This paper introduces a formal specification model that covers a large class of real flexible manufacturing system (FMS). Using this model, a designer expresses the functional capacities of his system and the product flows. Parallel manufacturing processes, having, transformation, assembly, disassembly, test and storage operations, are considered. FMS specification is automatically transformed into a CP-net model. Hence, the verification and the supervisory control techniques based on CP-nets can be applied to the generated CP-net. Thus, a parameterized solution is defined taking into account the flexibility of the specification model. The present work led to the implementation of a specific tool, called MAC-FMS, allowing graphical specification, supervisory control and verification through its interaction with CPN tools environment (Jensen's tool).
Abstract: In this paper, we present a controller synthesis method for resource allocation systems based on coloured Petri nets (CPN). The first contribution of this work is the use of High-level Petri nets as a basis model for the specification of the plant model as well as for the controller generation. Indeed, we present an automatic generation of a controller characterised by a CPN subnet (with a fixed number of places and transitions) representing its behaviour. The second contribution is the complete integration of the implementation of our method, called SACoRAS, in the CPN Tools. SACoRAS is made up of modules (graphical/textual editor, controller generator) that interact with CPN Tools modules (state space module, etc.).
