shown in Fig. 1. has a stochastic lifespan at "Send" state, FD-DEVS doesn't capture the non-determinism effectively. Tool For Verification There are two open source libraries DEVS# written in C# at http://xsy-csharp.sourceforge.net/DEVSsharp/ and XSY written in Python at https://code.google.com/p/x-s-y/ that support some reachability graph-based verification algorithms for finding safeness and liveness. For Simulation via XML For standardization of DEVS, especially using FDDEVS, Dr. Saurabh Mittal together with co-workers has worked on defining of XML format of FDDEVS. We can find an article at http://www.duniptechnologies.com/research/xfddevs/. This standard XML format was used for UML execution [RCMZ09] . Footnotes References [Dill89] D.L. Dill, "Timing Assumptions and Verification of Finite-State Concurrent Systems", In Proceedings of the Workshop on Computer Aided Verification Methods for Finite State Systems, pp 197-212, Grenoble, France, 1989 [Hwang05] M.H. Hwang, "Generating Finite-State Global Behavior of Reconfigurable Automation Systems: DEVS Approach", Proceedings of 2005 IEEE-CASE, Edmonton, Canada, Aug. 1-2, 2005(Available at http://moonho.hwang.googlepages.com/publications) [HZ06a] M. H. Hwang and Bernard Zeigler, "A Modular Verification Framework using Finite and Deterministic DEVS", Proceedings of 2006 DEVS Symposium, pp57-65, Huntsville, Alabama, USA, (Available at http://www.acims.arizona.edu ) [HZ06b] M. H. Hwang and Bernard Zeigler, "A Reachable Graph of Finite and Deterministic DEVS Networks", Proceedings of 2006 DEVS Symposium, pp48-56, Huntsville, Alabama, USA, (Available at http://www.acims.arizona.edu ) [HZ07] M.H. Hwang and Bernard Zeigler, "Reachability Graph of Finite & Deterministic DEVS", IEEE Transactions on Automation Science and Engineering,Volume 6, Issue 3, 2009, pp. 454–467, http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?isnumber=5153598&arnumber=5071137&count=19&index=7 [RCMZ09] José L. Risco-Martín, Jesús M. de la Cruz, Saurabh Mittal and Bernard Zeigler, "eUDEVS: Executable UML with DEVS Theory of Modeling and Simulation", SIMULATION, Transaction of The Society for Modeling and Simulation International,Volume 85, No. 11-12, 2009, pp. 750–777, http://sim.sagepub.com/content/85/11-12/750.short [ZKP00] Automata (computation)