Synthesis of Live Behaviour Models
Imperial College, London (UK)
Building 22 - Meeting Room
February 23rd, 2011
The design of reactive systems is a highly complex task requiring significant expertise. Consequently, it is highly desirable to have techniques that automatically generate by construction behaviour models satisfying a given set of requirements. We present a novel technique for synthesising behaviour models that works for safety and an expressive subset of liveness properties and conforms to the foundational requirements engineering World/Machine model, dealing explicitly with assumptions on environment behaviour and distinguishing controlled and monitored actions. This is the first technique that conforms to what is considered best practice in requirements specifications: distinguishing prescriptive and descriptive assertions. The technique offers a more realistic treatment of problem domains by allowing the integration of failures of controller actions in the environment model. Classical treatment of failures through strong fairness leads to a very high computational complexity and may be insufficient for many interesting cases. We identify a realistic stronger fairness condition on the behaviour of failures. We then identify sufficient conditions on the environment that ensure the resulting controller will be eager to satisfy its goals.
Nicolas D'Ippolito graduated from University of Buenos Aires with an MSc in Computer Science. After working for 7 years as a software engineer in various companies based in Buenos Aires, he began a PhD at Imperial College London under the supervision of Sebastian Uchitel and Nir Piterman. His research interests are mainly focused towards behavioural modelling, partial behavioural modelling, controller synthesis and model checking.
Advanced software architectures and methodologies