A formal framework for stochastic discrete event system specification modeling and simulation