Enhancing Stochastic Petri Nets with Reconfigurability (eBook)

Modeling, Analysis and Performance Evaluation

Samir Tigane, Laid Kahloul, Abdelhamid Mellouk (Autoren)

eBook Download: EPUB

2025
301 Seiten
Wiley-Iste (Verlag)
978-1-394-38865-3 (ISBN)

Infos

This book explores the world of reconfigurable stochastic Petri nets (RSPNs), a powerful method for modeling and verifying complex, dynamic and reconfigurable systems. As modern discrete-event systems become increasingly flexible, requiring structural adaptability at runtime, classical Petri nets are proving insufficient. This book presents innovative extensions to Petri nets, offering enhanced modeling capabilities for reconfigurable systems, while ensuring efficient verification.

Through a structured approach, this book introduces reconfigurable generalized stochastic Petri nets (RecGSPNs), an advanced framework that integrates reconfigurability while preserving crucial system properties such as liveness, boundedness and deadlock-freedom. This book systematically explores modeling techniques, including stochastic reward nets and dynamic topology transformations, demonstrating their effectiveness through quantitative and qualitative analyses. By addressing challenges in state-space explosion and computational complexity, this book provides essential methodologies for researchers and practitioners working on reconfigurable systems, and serves as a valuable resource for those working in network security, manufacturing systems and distributed computing, where dynamic reconfigurations are essential.

Samir Tigane is Associate Professor at the University of Biskra and researcher at the Laboratoire de l'Informatique Intelligente (LINFI), Algeria. His research includes software engineering, formal methods and artificial intelligence.

Laid Kahloul is Professor at the University of Biskra and researcher at the Laboratoire de l'Informatique Intelligente (LINFI), Algeria. His research includes software engineering, formal methods, security and artificial intelligence.

Abdelhamid Mellouk is Full-time University Professor, Director of the IT4H High School Engineering Department and Head of the TincNET Research Team, UPEC, France. He is also the founder of Network Control Research and Curricula activities at UPEC, President of the Policies and Programs commission at the National Council for Scientific Research and Technologies, a HCERES Expert, a CNU member and Co-President of the DS-AI Systematic Deep Tech Hub.

Textauszug

General Introduction

In this introduction, we start by presenting the background of this book, namely the formal modeling and verification based on dynamic-structure stochastic Petri nets. Then, we focus on the motivations of this work, specify the problem and the objectives and highlight our contributions. Finally, we end with the description of the manuscript organization.

I.1. Background

The major advancements in computing power, connectivity, sensors, storage capacity and software development have motivated companies as well as individuals to adopt and integrate IT solutions into their daily tasks (from a small device at the house to a gigantic infrastructure). As the list of advantages and benefits resulting from this orientation continues to grow, so do the risks of failure and malfunctioning that may threaten companies as well as individuals. Therefore, it is absolutely mandatory to ensure the proper functioning of computer systems according to customers’ and designers’ expectations. This concern had been identified since the late 1960s that marked the birth of software engineering. One of the main goals of the latter is enabling developers to implement complex systems that work properly. In this regard, several approaches have emerged to meet this crucial requirement in the various stages of the software life cycle (Woodcock et al. 2009).

Approaches in which the syntax, semantics and manipulation rules of specification language are explicitly defined by mathematics are called formal approaches. These approaches include Petri nets (Murata 1989), sequential process communication (SPC) (Brookes et al. 1984), LOTOS (Bolognesi and Brinksma 1987), B-method (Abrial 2005), etc. Actually, formal approaches allow a complete verification of the whole system behavior and prove the presence of certain desired properties for all possible inputs. By formal methods, we can write a formal specification of a system on which different properties can be proved, and thereafter we can mathematically prove that a system implementation meets this specification (Craigen et al. 1993; Haxthausen 2010; Garavel and Graf 2013; Rodhe and Karresand 2015). However, the use of formal methods does not guarantee a priori the accuracy of developed systems. Indeed, their use enhances our understanding of a system under construction while revealing its shortcomings, inconsistencies and ambiguities that might otherwise go unnoticed (Clarke and Wing 1996).

Among the most widespread formalisms, we find Petri nets (PNs) (Peterson 1977; Murata 1989). They are characterized by three major advantages (Peterson 1981; Kamath and Viswanadham 1986):

1. Modeling level: they have a powerful mathematical foundation, as well as an intuitive graphical representation. The graphical representation gives a flat view to PN models, making it possible to have simple and very explicit models. Also, their graphic modeling enables easy visualization of complex systems.
2. Verification level: their mathematical foundation is at the origin of all the analysis techniques that were proposed in order to verify the modeled systems. Indeed, they dispose of a well-developed qualitative/quantitative analysis panoply.
3. Coupling modeling and verification: they offer a careful balance of modeling and decision power. In fact, Petri nets have been used in the modeling of a wide variety of systems. As for their decision power, the reachability problem is decidable in Petri nets (note that most problems can be converted into reachability problems).

The model, in its origin proposed by “Adam Petri” in Petri (1962), that was initially concerned with describing the causal relationships between events that can occur in a computer system, has undergone significant evolution and adaptation to meet several requirements imposed by the appearance of new complicated systems. The most notable extensions can be found in four main categories:

• Colored PNs (Jensen 2013): each token becomes rather a distinguishable value from other tokens. The weights on the arcs are no longer constants, but rather mathematical functions that can be complicated. This model makes it possible to have models of reasonable size for complicated systems.
• Temporal PNs (Ramchandani 1973): the time introduced in PNs allows us to put explicit constraints on the dynamics of the model which reflect the real temporal constraints imposed on the system.
• Stochastic PNs (Marsan et al. 1994): stochastic PNs are a response to another missing realistic aspect in previous models, which is the aspect of hazard, randomness and non-absolute events. The random events in their arrivals will be explicitly considered and modeled, allowing the model to get closer to the real system and thus to have a good representation of the studied system.
• Reconfigurable PNs (Llorens and Oliver 2004b; Ehrig and Padberg 2004; Padberg and Kahloul 2018): this last category groups formalisms allowing the modeling of structure flexibility.

The purpose of this last variant is to provide a formal model for dynamic-structure systems, for example, flexible manufacturing systems (FMSs) (Buzacott and Shanthikumar 1980), reconfigurable manufacturing systems (RMSs) (Koren et al. 1999), production in cloud (Xu 2012), Industry 4.0 (Lasi et al. 2014), etc. In fact, many discrete event systems (DESs) are becoming increasingly complex, structurally dynamic and variably interconnected. These systems are designed to be able to change their structure and/or topology, at run time, by adding/removing interconnections, objects or even subsystems, to accommodate new circumstances/requirements. Ongoing studies on this class of systems focus on their key feature, namely, the reconfigurability (Brettel et al. 2014) that must occur at run time (i.e. dynamic reconfigurability) (Jackson et al. 2016). Dynamic reconfigurability is a critical activity that influences the performance, security and cost of such systems. To overcome the previous challenges, the designer must dispose of a rigorous approach and a set of appropriate tools.

The use of PNs in the study of such systems attracts many researchers (Silva and Valette 1990; Marsan et al. 1994; Recalde et al. 2004; Chen et al. 2017; Long et al. 2017; Latorre-Biel et al. 2018; Liu et al. 2018; You et al. 2018). In the literature, many classes of PNs have been proposed and applied to specify/verify reconfigurable systems. The chosen PN class is often motivated by the aspects to be specified and the properties to be verified. In fact, we can distinguish three classes of work: that uses basic PNs, that uses temporal or stochastic PNs and, finally, that applies reconfigurable PNs. Stochastic PNs (SPNs) and generalized SPNs (GSPNs) represent an extension of PNs (Marsan et al. 1994) used to model and evaluate stochastic systems. These formalisms allow the analysis of performance metrics such as productivity, energy consumption and machine utilization. Marsan et al. (1994) strongly emphasize the importance of GSPNs and SPNs as versatile design tools that fit well with the behavior of DESs at different stages of development (Long et al. 2015; Čapkovič 2017; Simon et al. 2018; Latorre-Biel et al. 2018). Although PNs (low or high) are a powerful and expressive tool, they are unable to specify/verify, in a natural way, advanced dynamic-structure systems (Capra and Camilli 2018). Systems supporting volatile environments, continuous variations and reconfigurable structures are expected to be extremely complex (Chryssolouris et al. 2013). The design of such systems is an increasingly complex and omnipresent challenge. Therefore, designers must dispose of the necessary approaches, models and tools to handle this complexity (Möller 2016). To overcome this issue, researchers introduce dynamic structures into PNs, thus expanding the standard formalism (Padberg and Kahloul 2018).

Rule-based graph transformations (Ehrig and Padberg 2004) offer a mathematically based graphical framework for modeling the reconfigurations in PN structures. Nevertheless, increasing the modeling power of a formalism decreases its decision power. Therefore, extensions proposed in the literature introducing reconfigurability to PNs try to find a compromise between the modeling and the verification levels. From this perspective, we can distinguish three main directions. On the one hand, researchers develop pre-processing techniques that encode, unfold or compile graphs and transformation rules into existing formalisms in order to exploit the panoply of their tools (Llorens and Oliver 2004b; Capra and Camilli 2018; Camilli et al. 2018). Although they can naturally model the reconfigurations, these approaches did not increase the modeling power compared to existing ones, since they depend on target formalisms expressiveness and in particular do not allow modeling infinite graphs (Rensink et al. 2004). For instance, classical model-checkers (Baier and Katoen 2008) use a fixed number of propositions, which prevents the modeling of infinite-structure systems (Rensink 2008). On the other hand, some techniques execute graph transformation systems and compute the reachability graph; nevertheless, an upper artificial threshold is still needed (Kastenberg and Rensink 2006). To mitigate this issue, some approaches compute either...

Produkt-Details

• Erscheint lt. Verlag: 17.6.2025
• Reihe/Serie: ISTE Invoiced
• Sprache: englisch
• Themenwelt: Technik ► Elektrotechnik / Energietechnik
• Schlagworte: boundedness • Computational Complexity • deadlock-freedom • Distributed Computing • Liveness • Manufacturing Systems • Modeling • Network Security • reconfigurability • reconfigurable stochastic Petri nets (RSPNs) • state-space explosion
• ISBN-10: 1-394-38865-9 / 1394388659
• ISBN-13: 978-1-394-38865-3 / 9781394388653