A Randomized Model for Communicating Embedded Systems

Nowadays, there is an intense research activity in designing systems that operate in real life, physical environments. This research is spanned by various areas in computer science and engineering: embedded systems, reactive systems, wireless communications, hybrid systems, stochastic processes, etc. A severe limitation in the development of these systems is due to the mathematical foundation and complexity of the physical environment. Often, the physical environment is continuous and uncertain, and modelled in terms of continuous stochastic processes. These mathematics are quite different from the underlying mathematics of discrete controllers based on logic and algebra. In this paper, we propose a specification formalism called stochastic functional logic based on algebraic framework. This axiomatises and abstracts away advanced structures from functional and stochastic analysis. The definition of the logic mimics the practice in applied mathematics. This logic is integrated with a probabilistic process algebra to provide a specification framework for embedded systems. The integration mechanism is based on partial ordered sets. Moreover, we construct an energy integral to every stochastic functional logic specification. In this way, we combine the power of formal specification and stochastic analysis for the software development of embedded systems.