System Behaviours and Problem Frames: Concepts, Concerns and the Role of Formalisms in the Development of Cyber-physical Systems.

Two salient issues in software engineering are the proper relationships of requirements to design and implementation and of formal to non-formal development techniques. Both of these issues are prominent in the development of software for cyber-physical systems-that is, for systems whose explicit purpose is to ensure desired effects and behaviours in the physical world. In such systems the software monitors and controls those parts of the world in which the desired effects and behaviours are located: the system behaviour is the result of this interaction between the machine and the problem world. In this paper these salient issues are addressed using the Problem Frames approach. Requirements are understood as desired properties of the system behaviour: design of the structure and content of that behaviour is the central development task. The relationship between formal and non-formal techniques is one of dependence: pre-formal development activities must precede the deployment of full formalisation and formal verification. These pre-formal activities embody the exploration, investigation and design that are an essential preliminary to formal work. They clarify the structure of system behaviour as an assemblage of constituent behaviours, separating the identification and study of those behaviours from the careful treatment of their interactions. In this way formal reasoning is accorded its proper role and an intellectual structure established within which it can play its due part in the development of dependable systems.