The BPMN standard notation allows business process designers to model both intra-organizational processes and inter-organizational collaborations. A great effort has been devoted in proposing formal ...semantics for BPMN, and, fewer, in providing dedicated verification tools. Still, some advanced features of BPMN, namely communication or time-related constructs, are often set aside. This becomes an issue as BPMN gains interest outside of its original scope, e.g., for the IoT where communication and time play an important role. In this paper, we propose a formal semantics for a subset of BPMN. This semantics takes into account not only the usual gateways, but also sub-processes, inter-process communication, and time-related constructs. In contrast to transformational approaches, which give a semantics to BPMN by mapping it to some formal model (e.g., transition systems or Petri nets), our approach is based on a direct formalization in first-order logic that is then realized in a straightforward way into the TLA+ formal language. We build on the TLA+ model-checker, TLC, to provide process designers with a verification framework, fbpmn, that one may use to check BPMN and workflow specific properties. Our tools and our model database are open source and freely available online.
•A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.•Automated verification of intra-organization workflows and inter-organization collaborations.•Seven models for communication, two models for time.•Communication models and properties of interest are easily extensible.•Open source and freely available tools and model repository.
The integration of the Internet of Things (IoT) paradigm into web services and cloud computing allows us to handle thousands of sensors and their data. In this regard, sensing as a service model has ...recently emerged and the data generated by these sensors can be reused by different users and applications within IoT middleware solutions. With the huge number of sensors available in the IoT environment, the crucial challenge is how to efficiently search and select the best sensors depending on the users’ requirements. This paper aims to exploit the power of a dynamic skyline operator in the field of multi-criteria decision making, to reduce the search space for the purpose of improving the efficiency of context-awareness and selecting the best sensors following the users’ request. The architecture adopted in this proposition is composed by several gateways distributed in the network and connected with a server, where each gateway must respond to user requests locally. Hereafter, the server will aggregate the results of all gateways and give the final answer. The experimentation shows the efficiency of our method in comparison to existing ones.
Nowadays, a wide range of systems are becoming structurally dynamic, variably interconnected, and highly complex. The use of classical formal approaches, such as Petri nets, in the design of such ...systems becomes neither convenient nor sufficient. Indeed, they cannot handle, in a natural way, the dynamic structure and the growing complexity of modern systems.
Introducing reconfigurability in Petri nets, as well as generalized stochastic Petri nets increases the modeling power, but decreases the applicability of analysis techniques. In fact, several properties become undecidable
In this paper, we extend generalized stochastic Petri nets to a reconfigurable formalism, while maintaining verifiability with reduced complexity. The proposed approach identifies a set of properties that are preserved after reconfiguration. These properties are decidable with reduced time and space complexity. The use of the proposed formalism is illustrated through a running example.
•A new Petri nets based formalism is proposed for reconfigurable systems.•The new formalism handles two aspects: stochastic time and reconfigurability.•Improved Net Rewriting Systems and Generalized Stochastic Petri Nets are combined.•A new approach for the performance evaluation is proposed and exploited.•The formalism is exploited in an Reconfigurable Manufacturing Systems case study.
one of the important challenges in wireless sensors networks (WSN) resides in energy consumption. In order to resolve this limitation, several solutions were proposed. Recently, the exploitation of ...mobile agent technologies in wireless sensor networks to optimize energy consumption attracts researchers. Despite their advantage as an ambitious solution, the itineraries followed by migrating mobile agents can surcharge the network and so have an impact on energy consumption. Many researches have dealt with itinerary planning in WSNs through the use of a single agent (SIP: Single agent Itinerary Planning) or multiple mobile agents (MIP: Multiple agents Itinerary Planning). However, the use of multi-agents causes the emergence of the data load unbalancing problem among mobile agents, where the geographical distance is the unique factor motivating to plan the itinerary of the agents. The data balancing factor has an important role especially in Wireless sensor networks multimedia that owns a considerable volume of data size. It helps to optimize the tasks duration and thus optimizes the overall answer time of the network. In this paper, we provide a new MIP solution (GIGM-MIP) which is based not only on geographic information but also on the amount of data provided by each node to reduce the energy consumption of the network. The simulation experiments show that our approach is more efficient than other approaches in terms of task duration and the amount of energy consumption.
The design and the evaluation of communication protocols in WSNs is a crucial issue. Generally, researchers use simulation methods to evaluate them. However, formal modelling and analysis techniques ...are an efficient alternative to simulation methods. Indeed, these techniques allow performance evaluation and model verification. In this paper, a formal approach is proposed to modelling and to evaluating the Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA) MAC protocol with a star topology. Moreover, the proposed approach deals with some properties that are not stated in most existing works. The approach uses Hierarchical Timed Coloured Petri Nets (HTCPNs) formalism to model the protocol and exploits the CPN-Tools to analyse the generated models. HTCPNs provide timed aspect which facilitates the consideration of time constraints inherent to the CSMA/CA protocol.
Role-Based Access Control (RBAC) is one of the most used models in designing and implementation of security policies, in large networking systems. Basic RBAC model does not consider temporal aspects ...which are so important in such policies. Temporal RBAC (TRBAC) is proposed to deal with these temporal aspects. Despite the elegance of these models, designing a security policy remains a challenge. Designers must ensure the consistency and the correctness of the policy. The use of formal methods provides techniques for proving that the designed policy is consistent. In this paper, we present a formal modelling/analysis approach of TRBAC policies. This approach uses Hierarchical Timed Coloured Petri Nets (HTCPN) formalism to model the TRBAC policy, and the CPN-tool to analyse the generated models. The timed aspect, in HTCPN, facilitates the consideration of temporal constraints introduced in TRBAC. The hierarchical aspect of HTCPN makes the model “manageable”, in spite of the complexity of TRBAC policy specification. The analysis phase allows the verification of many important properties about the TRBAC security policy.
Modern discrete-event systems (DESs) are often characterized by their dynamic structures enabling highly flexible behaviors that can respond in real time to volatile environments. On the other hand, ...timed automata (TA) are powerful tools used to design various DESs. However, they lack the ability to naturally describe dynamic-structure reconfigurable systems. Indeed, TA are characterized by their rigid structures, which cannot handle the complexity of dynamic structures. To overcome this limitation, we propose an extension to TA, called dynamic timed automata (DTA), enabling the modeling and verification of reconfigurable systems. Additionally, we present a new algorithm that transforms DTA into semantic-equivalent TA while preserving their behavior. We demonstrate the usefulness and applicability of this new modeling and verification technique using an illustrative example.
Celotno besedilo
Dostopno za:
DOBA, IZUM, KILJ, NUK, PILJ, PNG, SAZU, UILJ, UKNU, UL, UM, UPUK
Existing medium access control (MAC) protocols have always considered the energy-harvesting aspect and mobility aspect separately. Thus, in literature, there is no MAC protocol that has combined the ...two aspects in the same framework to improve networks performance. In this paper, a new “Mobility and Energy Harvesting aware Medium Access Control (MEH-MAC)” protocol is proposed for dynamic sensor networks powered by ambient energy. The paper provides a detailed description of the protocol and presents a state-transition formal model with a performance evaluation using UPPAAL-SMC.
PDF
