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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 email@example.com
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 firstname.lastname@example.org