Model-Based Specification and Refinement for Cyber-Physical Systems

Cyber-physical systems are small yet powerful systems which are embedded into their environment, adapting to its changes and at the same controlling it, and often operating autonomously. These systems have reached a level of complexity that opens up new application areas, but at the same time strains the existing design flows in system development. To ameliorate this problem, we propose a novel design flow for cyber-physical systems by adapting model-based specification and refinement methods known from software development. The design flow allows to start with a system specification and its essential properties at a high level of abstraction, and gradually refines it down to an electronic system level. Properties of higher levels can be inherited during refinements to lower levels by relying on local proof obligations only, which results in a design flow capable to keep up with the increasing complexity of cyber-physical systems.