Keywords: Verification, validation, test, Modeling tools: Petri nets, automata, ..., Applications
Abstract: Formalisms such as IEC 60848 GRAFCET can be used for the specification of system behavior, as a basis for verification, and for automated code generation, e.g. to Structured Text (ST) according to IEC 61131-3. A possible procedure comprises the specification of the system, the verification of that model followed by automated code generation. However, the verification results can be rendered useless if the automated code generator introduces unintended, possibly faulty behavior. This paper discusses an approach of verifying the generated code in ST against its original specification in GRAFCET using model checking, using an existing code generator.

Keywords: Modeling tools: Petri nets, automata, ..., Supervisory Control Theory, Applications
Abstract: This paper presents the modeling and a formal verification approach of energy management control systems for microgrids subject to unknown demand and uncertainties in the availability of renewable energy sources. The main objective of this study is to develop a management system for a microgrid composed of renewable and non-renewable energy sources, specifying the different possible modes. A supervisory control method is proposed to autonomously control and monitor a microgrid and maintain more stable energy flows with maximum utilization of available resources. A timed automata network model of the microgrid has been developed by modeling the dynamics of components such as PV, BESS, diesel generator, load, and controller. Possible operating modes in the microgrid between sources and load are derived and classified into allowed and unallowed operating modes. Verification of the designed microgrid models was performed using simulation and formal methods. The advantageous performance of the proposed strategy is illustrated via a numerical example.

Keywords: Discrete approaches for hybrid systems, Applications
Abstract: We present a discrete-event system formalism to capture experimentally observed activity of genes in single cells, where a gene can stochastically switch between an active state (synthesis of gene products, such as mRNA and proteins) and an inactive state (synthesis is turned OFF). Extending prior work that focused on memory-less switching kinetics, this contribution extends the models considering the time spent in each state to be an arbitrary positively-valued random variable. Here, memory-based switching is captured via the introduction of molecular timers that measure the time spent in a state, and switching rates are timer-dependent. Hence, a gene is more likely to turn OFF if it has been active for a long period. We provide exact analytical derivations of the mean and extent of stochasticity in the gene product level for these models and systematically study how different model parameters can be calibrated to attenuate or amplify noise in gene expression. These results can be combined with experimental data on measured levels inside individual cells to gain valuable insights into the gene expression process across different cell types, from bacterial to human cells.

Keywords: Verification, validation, test, Supervisory Control Theory, Modeling tools: Petri nets, automata, ...
Abstract: Smart contracts are programs stored on a blockchain ledger, thus being immutable after deployment, which makes assessment of their correctness before deployment vital. Extended finite state machines (EFSM) offer a structured framework for modeling complex systems, thus providing a systematic approach to scrutinize smart contract functionalities. This paper describes a methodology to automatically convert from the abstract syntax tree of a smart contract to an EFSM model. A smart contract implementing a casino is the specific use case, and verification of the EFSM model reveals it to be blocking. This blocking represents that a malicious player can lock the funds of the casino so that they can never be retrieved.

Keywords: Supervisory Control Theory, Modeling tools: Petri nets, automata, ..., Tools
Abstract: A large number of ship locks in the Netherlands require renovation. This paper focuses on the application of the synthesis-based engineering (SBE) in the design of supervisory controllers for ship locks, to achieve correct-by-construction control software. A configurator for SBE models for supervisor synthesis is proposed, based on parameters describing the mechanical composition. The accompanying tool, which supports model simulation, demonstrates improvement in time, quality and human error avoidance, and is already being used in the design of ship lock supervisors in Lelystad and Maasbracht. The tool was designed for ship locks but the structure of the tool allows adaptation for other families of systems.

Keywords: Modeling tools: Petri nets, automata, ..., Diagnosis, fault tolerance, observability, ...
Abstract: This paper focuses on the modeling and estimation of the timing behavior of discrete manufacturing systems modeled by signal interpreted Petri nets (SIPN). At first, in order to take into account the temporal behavior of the plant, the concept of SIPN is extended to time signal interpreted Petri nets (TSIPN). Then, a state estimation approach based on the TSIPN model is developed to deliver the information about the current state of the plant by using online measurements. Finally, it is shown how the results of the state estimation can be used to predict future states of the manufacturing system. The proposed approaches are characterized by their practical relevance and their low computational complexity. Examples of a heated mixing tank system are given to illustrate the main results.

Keywords: Modeling tools: Petri nets, automata, ..., Applications, Algebraic approaches: process algebras, max/plus-algebra, ...
Abstract: Time-Sensitive Networking (TSN) is a set of standards designed to provide determinism to Ethernet or wireless networks for real-time applications. Network Calculus (NC) is the best-known formal tool for TSN analysis, but it is hard to apply in scenarios of changing conditions. Petri Nets can potentially overcome some limitations of NC, but they have rarely been used as an analytical tool for TSN. This work presents a novel modeling methodology exploiting Timed Continuous Petri Nets (TCPNs) to abstract and analyze TSN nodes.

Keywords: Modeling tools: Petri nets, automata, ..., Applications
Abstract: Green supply chain is an emerging approach in supply chain management to reduce environmental impact of the process concerning the flow of goods and materials. As a discrete- event system, supply chain can be modeled using Petri Nets. Colored Petri Nets (CPNs) extend the classical Petri net formalism with data, time and hierarchy. These extensions makes it possible to deal with the green aspects of the supply chain. This paper deals with the Colored Petri Net approach to model and simulate a green supply chain system. The forward supply chain network starts from the raw material suppliers, to the manufacturers, wholesalers, retailers and to the final customers. The reverse supply chain network is made of collecting points, recycling plants, disassembly plants,and secondary material market. A government environment agency plays the role of regulation of the recycling process. A colored Petri net model of the green supply chain is developed and simulated with CPN Tools, a dedicated software for CPN models. The simulation results as well as the state-space analysis results validate the correctness of the model.

Keywords: Modeling tools: Petri nets, automata, ..., Supervisory Control Theory
Abstract: This work introduces a framework to describe and control collaborative systems in a distributed manner. Within this framework, both a set of agents and a specification to be accomplished are modelled using Interpreted Petri nets. The agents' output states are partially known, and the specification describes a subset of relevant states to be reached by the agents without explicitly detailing which agents are involved in achieving such specification or the precise states that each agent must reach individually. This framework enables agents to collaboratively discover how to fulfill a shared, high-level specification, even in the absence of detailed instructions. The approach promises to enhance scalability, flexibility, and efficiency in collaborative settings. For illustrative purposes, a simplified collaborative assembly system is showcased to demonstrate the proposed framework.

Keywords: Tools, Modeling tools: Petri nets, automata, ...
Abstract: Simuleau is a modeling, analysis and simulation tool for discrete event models expressed by batches Petri nets, a formalism that enriches hybrid Petri nets of David and Alla. Batches PNs incorporate timed-transition discrete PNs, constant continuous PNs, and new types of nodes called batch nodes. This formalism and Simuleau have been exploited among diverse application areas such as manufacturing systems, communication networks, and traffic road. After presenting batches PN formalisms and their application domains, this paper focuses on the main characteristics of Simuleau, including the tool structure, its menu interface, the input model description and the outputs obtained after simulation.