Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions

Hayes, Ian J. (2014). Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. In: Cyrille Artho and Peter Csaba Olveczky, Formal Techniques for Safety-Critical Systems - 2nd International Workshop, FTSCS 2013, Revised Selected Papers. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013, Queenstown, (1-2). 29 - 30 October 2013. doi:10.1007/978-3-319-05416-2_1


Author Hayes, Ian J.
Title of paper Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions
Conference name 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013
Conference location Queenstown
Conference dates 29 - 30 October 2013
Proceedings title Formal Techniques for Safety-Critical Systems - 2nd International Workshop, FTSCS 2013, Revised Selected Papers   Check publisher's open access policy
Journal name Communications in Computer and Information Science   Check publisher's open access policy
Series Communications in Computer and Information Science
Publication Year 2014
Year available 2014
Sub-type Fully published paper
DOI 10.1007/978-3-319-05416-2_1
Open Access Status
ISBN 9783319054155
9783319054162
ISSN 1865-0929
1865-0937
Editor Cyrille Artho
Peter Csaba Olveczky
Volume 419
Start page 1
End page 2
Total pages 2
Chapter number 1
Total chapters 18
Collection year 2015
Language eng
Abstract/Summary 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 then 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.
Q-Index Code EX
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 12 Aug 2014, 04:39:13 EST by System User on behalf of School of Information Technol and Elec Engineering