报 告 人：Richard Banach (英国曼切斯特大学副教授)
邀 请 人：苏雯 博士
In the effort to develop critical cyberphysical systems, existing computing formalisms are extended to include continuous behaviour. This may happen in a way that neglects elements necessary for correct continuous properties and correct physical properties. A simple language is taken to illustrate this. Issues and risks latent in this kind of approach are identified and discussed under the umbrella of `healthiness conditions'. Modifications to the language in the light of the conditions discussed are described. An example air conditioning system is used to illustrate the concepts presented, and is developed both in the original language and in the modified version.
Richard Banach received the degree of B.Sc. in Mathematical Physics from Birmingham University (UK). This was followed by a Diploma in Advanced Studies in Science and by a Ph.D. in Theoretical Physics, both from Manchester University (UK). The field of study for his doctorate was quantum field theory in topologically non-trivial spacetimes. Most recently, the increasing popularity of real-world systems that contain components that interact with the physical world, so-called cyberphysical systems, has led to a redirection of the existing formal methods interests towards methodologies for the top-down design and development of such systems. Dr. Banach regularly acts as a reviewer for work in the formal methods area, and is a Foundation Editor of the Journal of Universal Computer Science.