Hdl Handle:
http://hdl.handle.net/10149/91097
Title:
Editorial
Authors:
Paige, R. F. (Richard); Brooke, P. J. (Phillip)
Affiliation:
University of Teesside. School of Computing.
Citation:
Paige, R. F. and Brooke, P. J. (2009) 'Editorial', Formal Aspects of Computing, 21 (4), p.303.
Publisher:
Springer
Journal:
Formal Aspects of Computing
Issue Date:
Aug-2009
URI:
http://hdl.handle.net/10149/91097
DOI:
10.1007/s00165-009-0113-z
Abstract:
The authors present a Special Issue on Concurrency and Real-Time for Eiffel-like Languages. The papers in this special issue originate from a workshop held in York, U.K., in July 2006. The workshop was organised by the University of York, the University of Teesside and ETH Z¨ urich. It was sponsored by the ARTIST Network of Excellence on Embedded Systems Design (http://www.artist-embedded.org) and supported by Formal Methods Europe. The workshop proceedings (consisting of nine fully refereed and revised papers, three invited papers, and one invited tutorial) appeared as a University of York technical report. After the workshop, presenters were invited to submit substantially revised and extended papers for inclusion in this special issue. As a result, four papers were accepted and are included herein. Two of the papers are concerned with the relationship between contracts (pre- and postconditions of routines that belong to classes, and invariants of classes themselves) and concurrency, and the semantic issues associated with their formalisation, reasoning, and implementation. “Contracts for Concurrency” by Nienaltowski, Meyer and Ostroff presents a new semantics for contracts that applies equally well to sequential and concurrent object-oriented programming. The semantics itself is argued to be a generalisation of traditional correctness semantics for object-orientation, and proof techniques are presented. “Beyond Contracts for Concurrency”, by Ostroff, Torshizi, Huang and Schoeller, shows how theorem proving that is useful for sequential object-oriented programming can also be used in a concurrent setting, using a Hoare-style logic. For system properties (such as liveness), a virtual machine is described that makes it feasible to use model checking to verify these properties. “FlexibleAccessControl Policy for SCOOP” by Nienaltowski addresses a challenging problemwithin concurrent object-oriented programming: how to reduce the amount of locking that is necessary to ensure correctness, so as to increase the amount of parallelism. Nienaltowski presents a formal lock passing mechanism (which is implemented in the current version of concurrent Eiffel) and demonstrates how it improves expressiveness and reduces the risk of deadlock. Finally, “Cameo: an Alternative Model of Concurrency for Eiffel” by Brooke and Paige presents a new concurrency model for Eiffel-like languages, where it is argued that the new model provides increased clarity and parallelism but also increases overhead due to lock management. A CSP formalisation of the model is provided. We thank John Cooke for supporting us in publishing the collection of papers contained in this journal, and for his help through the reviewing and editorial process. We also thank the participants of the workshop, the workshop program committee, and all of the reviewers involved in selecting the papers.
Type:
Article
Language:
en
Keywords:
concurrency; real-time; Eiffel; languages
ISSN:
09345043; 1433299X
Rights:
Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 03/02/2010]
Citation Count:
0 [Scopus, 03/02/2010]

Full metadata record

DC FieldValue Language
dc.contributor.authorPaige, R. F. (Richard)en
dc.contributor.authorBrooke, P. J. (Phillip)en
dc.date.accessioned2010-02-03T12:29:19Z-
dc.date.available2010-02-03T12:29:19Z-
dc.date.issued2009-08-
dc.identifier.citationFormal Aspects of Computing; 21 (4): 303en
dc.identifier.issn09345043-
dc.identifier.issn1433299X-
dc.identifier.doi10.1007/s00165-009-0113-z-
dc.identifier.urihttp://hdl.handle.net/10149/91097-
dc.description.abstractThe authors present a Special Issue on Concurrency and Real-Time for Eiffel-like Languages. The papers in this special issue originate from a workshop held in York, U.K., in July 2006. The workshop was organised by the University of York, the University of Teesside and ETH Z¨ urich. It was sponsored by the ARTIST Network of Excellence on Embedded Systems Design (http://www.artist-embedded.org) and supported by Formal Methods Europe. The workshop proceedings (consisting of nine fully refereed and revised papers, three invited papers, and one invited tutorial) appeared as a University of York technical report. After the workshop, presenters were invited to submit substantially revised and extended papers for inclusion in this special issue. As a result, four papers were accepted and are included herein. Two of the papers are concerned with the relationship between contracts (pre- and postconditions of routines that belong to classes, and invariants of classes themselves) and concurrency, and the semantic issues associated with their formalisation, reasoning, and implementation. “Contracts for Concurrency” by Nienaltowski, Meyer and Ostroff presents a new semantics for contracts that applies equally well to sequential and concurrent object-oriented programming. The semantics itself is argued to be a generalisation of traditional correctness semantics for object-orientation, and proof techniques are presented. “Beyond Contracts for Concurrency”, by Ostroff, Torshizi, Huang and Schoeller, shows how theorem proving that is useful for sequential object-oriented programming can also be used in a concurrent setting, using a Hoare-style logic. For system properties (such as liveness), a virtual machine is described that makes it feasible to use model checking to verify these properties. “FlexibleAccessControl Policy for SCOOP” by Nienaltowski addresses a challenging problemwithin concurrent object-oriented programming: how to reduce the amount of locking that is necessary to ensure correctness, so as to increase the amount of parallelism. Nienaltowski presents a formal lock passing mechanism (which is implemented in the current version of concurrent Eiffel) and demonstrates how it improves expressiveness and reduces the risk of deadlock. Finally, “Cameo: an Alternative Model of Concurrency for Eiffel” by Brooke and Paige presents a new concurrency model for Eiffel-like languages, where it is argued that the new model provides increased clarity and parallelism but also increases overhead due to lock management. A CSP formalisation of the model is provided. We thank John Cooke for supporting us in publishing the collection of papers contained in this journal, and for his help through the reviewing and editorial process. We also thank the participants of the workshop, the workshop program committee, and all of the reviewers involved in selecting the papers.en
dc.language.isoenen
dc.publisherSpringeren
dc.rightsAuthor can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 03/02/2010]en
dc.subjectconcurrencyen
dc.subjectreal-timeen
dc.subjectEiffelen
dc.subjectlanguagesen
dc.titleEditorialen
dc.typeArticleen
dc.contributor.departmentUniversity of Teesside. School of Computing.en
dc.identifier.journalFormal Aspects of Computingen
ref.citationcount0 [Scopus, 03/02/2010]en
or.citation.harvardPaige, R. F. and Brooke, P. J. (2009) 'Editorial', Formal Aspects of Computing, 21 (4), p.303.-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.