Invited talk: Ian Hayes
School of ITEE, The University of Queensland, Brisbane, Australia
Towards structuring system specifications with time bands using layers of rely-guarantee conditions
The overall specification of a cyber-physical system can be given in terms of the desired behaviour of its physical components operating within the real world. The specification of its control software can then be derived from the overall specification and the properties of the real-world phenomena, including their relationship to the computer system's sensors and actuators. The control software specification them becomes a combination of the guarantee it makes about the system behaviour and the real-world assumptions it relies upon.
Such specifications can easily become complicated because the complete system description deals with properties of phenomena at widely different time granularities, as well as handling faults. To help manage this complexity, we consider layering the specification within multiple time bands, with the specification of each time band consisting of both the rely and guarantee conditions for that band, both given in terms of the phenomena of that band. The overall specification is then the combination of the multiple rely-guarantee pairs. Multiple rely-guarantee pairs can also be used to handle faults.
Bio
Ian Hayes is a Professor in the School of Information Technology and Electrical Engineering at the University of Queensland, Australia. His research interests focus on methods for specifying and reasoning about software and systems. Recent research includes methods for reasoning about concurrent programs in a rely-guarantee style that emphasises the algebraic properties of parallelism and guarantee and rely constructs. A long-term theme of his research has looked at real-time systems. Recently this has examined structuring system specifications using time bands, while earlier research focussed on refinement of real-time systems. His earlier research while at Oxford University focussed on software specification using Abrial's Z specification language.