The Library
Responsiveness of interoperating components
Tools
UNSPECIFIED (2004) Responsiveness of interoperating components. FORMAL ASPECTS OF COMPUTING, 16 (4). pp. 394-411. doi:10.1007/s00165-004-0050-9 ISSN 0934-5043.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1007/s00165-004-0050-9
Abstract
This paper investigates the issue of responsiveness of interoperating components: one not causing the other to deadlock. This is obviously related to the question of whether the two deadlock when put in parallel. However, it is different in that we require that a specific process P is not itself blocked by a plugin Q when it could otherwise have progressed, instead of asking that either process can always proceed (deadlock freedom). The issue becomes yet more subtle when dealing with processes which can nondeterministically block, either through graceful termination or unfortunate deadlock. The relational predicate, that is, binary relation on processes, which we provide is refinement-closed. This is significant as it allows components to be developed independently. In addition, it can be mechanically verified. The contribution of this paper is to identify the issue of responsiveness; to define appropriate properties; to demonstrate the suitability of these properties and consider how they can be mechanically verified. The notation used is CSP with automatic model-checking provided by the FDR tool.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Journal or Publication Title: | FORMAL ASPECTS OF COMPUTING | ||||
Publisher: | SPRINGER | ||||
ISSN: | 0934-5043 | ||||
Official Date: | November 2004 | ||||
Dates: |
|
||||
Volume: | 16 | ||||
Number: | 4 | ||||
Number of Pages: | 18 | ||||
Page Range: | pp. 394-411 | ||||
DOI: | 10.1007/s00165-004-0050-9 | ||||
Publication Status: | Published |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |