China 
Africa 
Explore chapters and articles related to this topic
Equivalence Checking
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC Implementation, Circuit Design, and Process Technology, 2018
Andreas Kuehlmann, Fabio Somenzi
Reachability analysis computes the states of a sequential machine M that either are reachable from a set of designated states, or from which the designated states are reachable. In equivalence verification, the states reachable from the initial states form the strongest possible ϱ: the outputs of M1 and M2 agree in all reachable states of M = M1 × M2 if and only if M1 is equivalent to M2. Conversely, the complement of the states from which miscomparing states can be reached form the weakest ϱ for which the “if and only if” condition holds. The two cases corresponds to forward and backward reachability analysis, respectively. We first discuss forward analysis, and then briefly outline the differences.
Principles of DEVS Model Verification for Real-Time Embedded Applications
Published in Katalin Popovici, Pieter J. Mosterman, Real-Time Simulation Technologies, 2017
Hesham Saadawi, Gabriel A. Wainer, Mohammad Moallemi
The work by Hernandez and Giambiasi [20] showed that the verification of general DEVS models through reachability analysis is undecidable. The authors based their deduction on building a DEVS simulation Turing machine. Since the halting problem in Turing machines is undecidable (i.e., with analysis only, we cannot know in which state a Turing machine would be), they concluded that this is also true for DEVS models. In other words, we cannot recognize if we have reached a particular state starting from an initial state, and consequently, reachability analysis for general DEVS is impossible. Based on this result, reachability analysis may be possible only for restricted classes of DEVS. This result was based on introducing state variables with infinite number of values into the DEVS formalism. Therefore, limiting the number of states of a DEVS model is mandatory for decidable reachability. Hence, further work [21] introduced a new class of DEVS called time-constrained DEVS (TC-DEVS), which expanded the definition of DEVS atomic models with multiple clocks incremented independently of other clocks. Classic DEVS atomic models can be seen as having only one clock that keeps track of the elapsed time in a state and is reset on each transition. TC-DEVS also added clock constraints similar to TA (to function as guards on external and internal transitions). However, it is different from UPPAAL TA in that it allows clock constraints in state invariants to include clock differences. TC-DEVS is then transformed into an UPPAAL TA model. This work, however, did not include a transformation of TC-DEVS state invariants to UPPAAL TA when the model has invariants with clock differences, as this is not allowed in UPPAAL TA.
Dimensioning of Civilian Avionics Networks
Published in Richard Zurawski, Industrial Communication Technology Handbook, 2017
Jean-Luc Scharbarg, Christian Fraboul
A system modeled with timed automata can be verified using a reachability analysis that is performed by model checking. It consists in encoding each property in terms of the reachability of a given node of one of the automata.
Topological reverse mirroring: a new efficient knowledge-based methodology of reachability analysis for Petri nets
Published in International Journal of Control, 2022
Petri nets (PNs) have been widely applied for modelling and analysing concurrent systems, such as resource allocation (or flexible manufacturing) systems (RAS) (or FMS) (Chao, 2005, 2006, 2011a, 2011b, 2012; Ezpeleta et al., 1995; Huang et al., 2021; Lee et al., 2005; Li, Liu, et al., 2012; Luo et al., 2018; Shih & Chao, 2009; Sun et al., 2011; Uzam & Zhou, 2006; Yang et al., 2018; Zhou et al., 2019; Zimmermann, 2013). Reachability analysis (Ferrarini, 1994; Hiraishi & Ichikawa, 1988; Ichikawa et al., 1985; Kostin, 2003; Lee et al., 1990; Li et al., 2018; Lu et al., 2019; Miyamoto & Horiguchi, 2011; Mizuno et al., 2007; Wang et al., 2018) can be used to verify system properties of boundedness, liveness, reversibility, and so on. However, the persistent problem of using PNs to model very large systems is the large number of states generated (called the state explosion problem). Lee et al. (1990) have shown that the complexity of the reachability problem of PNs is EXPSPACE-hard and also (whether a marking is reachable) is NP-complete.
Fault detection and isolation using viability theory and interval observers
Published in International Journal of Systems Science, 2018
Majid Ghaniee Zarch, Vicenç Puig, Javad Poshtan, Mahdi Aliyari Shoorehdeli
Reachability analysis identifies the set of states backward (forward) reachable by a constrained dynamical system from a given target (initial) set of states. The notions of maximal and minimal reachability analysis were introduced in Mitchell (2007). Their corresponding constructs differ in how the time variable and the bounded input are quantified. In the formation of the maximal reachability construct, the inputs try to steer as many states as possible to the target set. On the other hand, in the formation of the minimal reachability construct, the trajectories reach the target set regardless of the input applied. Based on these differences, the maximal and minimal reachable sets and tubes (the set of states traversed by the trajectories over the time horizon (Mitchell, 2007)) are formed.