The usage of stochastic processes in embedded system specifications

We review the use of nondeterminism and identify two different purposes. The descriptive purpose handles uncertainties in the behaviour of existing entities. The constraining purpose is used in specifications to constrain implementations. For the specification of embedded systems we suggest a stochastic process σ instead of nondeterminism. It serves mostly the descriptive purpose but can also be used to constrain the system. We carefully distinguish different interpretations of these concepts by the different design activities simulation, synthesis and verification