An Integrated Specification Logic for Cyber-Physical Systems

Cyber-physical systems denote a new modeling paradigm that promotes a holistic view on complex systems. These systems have been studied before from various particular perspectives using paradigms like ubiquitous and distributed computing or embedded and hybrid systems. In modeling cyber-physical systems one has to consider the interaction between physics, computation and communication (networking), and a formal framework to study this systems has to be invented. In this paper we develop a formal approach called Hilbertean formal methods to provide a denotational semantics for cyber-physical systems. We combine denotational semantics with an algebraic model for physical processes to model physical causality and observability.