enter search term and/or author name
Introduction to the Special Issue on Modeling and Verification of Discrete Event Systems
Mohamed Khalgui, Zhiwu Li
Article No.: 1
Design of Liveness-Enforcing Supervisors for S3PR Based on Complementary Places
Shouguang Wang, Chengying Wang, Yanping Yu
Article No.: 2
In this article, an algorithm is proposed to design liveness-enforcing supervisors for systems of simple sequential processes with resources (S3PR) based on complementary places. Firstly, a mixed integer programming (MIP) based deadlock...
Computation of Minimal Siphons in Petri Nets by Using Binary Decision Diagrams
Yufeng Chen, Gaiyun Liu
Article No.: 3
Siphons play an important role in the development of deadlock control methods by using Petri nets. The number of siphons increases exponentially with respect to the size of a Petri net. This article presents a symbolic approach to the computation...
Design, Analysis and Verification of Real-Time Systems Based on Time Petri Net Refinement
Zhijun Ding, Changjun Jiang, Mengchu Zhou
Article No.: 4
A type of refinement operations of time Petri nets is presented for design, analysis and verification of complex real-time systems. First, the behavior preservation is studied under time constraints in a refinement operation, and a sufficient...
Modeling and Analysis of TinyOS Sensor Node Firmware: A CSP Approach
Allan I. McInnes
Article No.: 5
Wireless sensor networks are an increasingly popular application area for embedded systems. Individual sensor nodes within a network are typically resource-constrained, event-driven, and require a high degree of concurrency. This combination of...
This article deals with the formal validation of STIMAP, a medium access protocol that has been designed to meet the specific requirements of an implantable network-based neuroprosthesis. This article presents the modeling and the validation of...
Reducing Interleaving Semantics Redundancy in Reachability Analysis of Time Petri Nets
Hanifa Boucheneb, Kamel Barkaoui
Article No.: 7
The main problem of verification techniques based on exploration of (reachable) state space is the state explosion problem. In timed models, abstract states reached by different interleavings of the same set of transitions are, in general,...
Sequence Control of Essential Siphons for Deadlock Prevention in Petri Nets
Zhiming Zhang, Weimin Wu
Article No.: 8
Deadlock prevention is crucial to the modeling of flexible manufacturing systems. In the Petri net framework, deadlock prevention is often addressed by siphon-based control (SC) policies. Recent research results show that SC methods can avoid full...
A Hybrid Genetic Algorithm for the Bottleneck Traveling Salesman Problem
Zakir Hussain Ahmed
Article No.: 9
The bottleneck traveling salesman problem is to find a Hamiltonian circuit that minimizes the largest cost of any of its arcs in a graph. A simple genetic algorithm (GA) using sequential constructive crossover has been developed to obtain...
One-Step Look-Ahead Maximally Permissive Deadlock Control of AMS by Using Petri Nets
Naiqi Wu, Mengchu Zhou, Gang Hu
Article No.: 10
It is desired that a deadlock control policy for automated manufacturing systems (AMS) is maximally permissive. However, its tractability issue remains open, and this work addresses this important issue. It models AMS with a resource-oriented...
Transition-Based Deadlock Detection and Recovery Policy for FMSs Using Graph Technique
Yi-Sheng Huang, Yen-Liang Pan, Pin-June Su
Article No.: 11
A transition-controlled deadlock detection and recovery prevention policy is presented for a subclass of Petri nets used to model flexible manufacturing systems. The subclass is called systems of simple sequential processes with resources...
Fault Modeling in Discrete Event Systems Using Petri Nets
Payam Nazemzadeh, Abbas Dideban, Meisam Zareiee
Article No.: 12
In this article a model-based controller reconfiguration method for fault-tolerant control of discrete event systems has been introduced. In this method, we model the fault conditions for each specified fault as a new model called fault model. The...
Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL
Tarek Mhamdi, Osman Hasan, Sofiène Tahar
Article No.: 13
Dynamic systems that exhibit probabilistic behavior represent a large class of man-made systems such as communication networks, air traffic control, and other mission-critical systems. Evaluation of quantitative issues like performance and...
Formal Specification of Medical Systems by Proof-Based Refinement
Dominique Méry, Neeraj Kumar Singh
Article No.: 15
Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based...
Combining Formal Methods for the Development of Reactive Systems
Article No.: 16
This article deals with the use of two verification approaches: theorem proving and model checking. We focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA+ by using its model...
Formal Verification of Downtimeless System Evolution in Embedded Automation Controllers
Christoph Sünder, Valeriy Vyatkin, Alois Zoitl
Article No.: 17
This article presents a new formal approach to validation of on-the-fly modification of control software in automation systems. The concept of downtimeless system evolution (DSE) is introduced. The DSE is essentially based on the use of IEC 61499...
Distributed Reconfigurations of Autonomous IEC61499 Systems
Article No.: 18
The article deals with Distributed Multiagent Reconfigurable Embedded Control Systems following the International Industrial Standard IEC61499 in which a Function Block (Abbreviated by FB) is an event-triggered software component owning data and a...