A unifying specification logic for cyber-physical systems

The varieties of possible interaction between computational systems and physical environments is at the heart of a new modeling paradigm called cyber-physical systems. In order to model and control these interactions it necessary to present the fundamental properties of physical environments in a formalism compatible with the computational structures, usually in a formal logic or an algebraic calculus. In this paper, we propose a model as a step towards reasoning about the problems of uncertainty and surprise in the context of cyber-physical systems operating under mixed human/autonomous control. In controlling embedded devices, human operators are, in most cases, assisted by automated controllers (like driving assistance systems and automatic pilots). A new issue appeared in many applications is to model the automatic controllers which are user centric, i.e. the controllers are carrying a runtime monitoring of the system behaviour in its environment, they inform and warn the user on safety hazardous situation and they take action only when the user fails to react. A robust controller should be able to operate in open, random environments and to assist the human operator in case of appearance of surprising, possible catastrophic situations.