Title: Engineering Emergent Behaviour Time: 14:00-16:00 on Sept. 3th, 2009 (Thursday) Abstract: Recently the name ‘ensemble’ has been given to any information system that is complex enough to exhibit emergent behaviour: behaviour that is not a result of its components in isolation. Examples include the web and other large systems of agents which adapt to their open environment. Characteristic properties of an ensemble include a massive number of components and behaviour that is not just emergent, but also open, adaptive and statistical. But if an ensemble exhibits emergent behaviour, how can it be engineered using the techniques founded on Formal Methods that we use currently for the engineering of information systems? Indeed at least four papers claim independently that to be impossible, one quoting the glider in Conway's Game of Life as an example that cannot be developed by Formal Methods. In this talk we take the opposite view, and show how the glider can be developed using Formal Methods. The result is a methodology for Ensemble Engineering.
Abstract: If read and write operations are performed on the same memory cell at the same time, which is called a race, read operation may obtain an erroneous value. Wait-free algorithms have been studied that can implement read and write operations correctly, including race-free. In this talk, we will discuss how classic assertional reasoning methods can be used to verify one such algorithm, due to Simpson. |
