Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/8818
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Hierons, RM | - |
dc.contributor.author | Núñez, M | - |
dc.date.accessioned | 2014-08-04T11:18:29Z | - |
dc.date.available | 2014-08-04T11:18:29Z | - |
dc.date.issued | 2012 | - |
dc.identifier.citation | Formal Aspects of Computing, 24(4), 679 - 699, 2012 | en_US |
dc.identifier.issn | 0934-5043 | - |
dc.identifier.uri | http://link.springer.com/article/10.1007%2Fs00165-012-0244-5 | en |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/8818 | - |
dc.description | This is the author's accepted manuscript. The final publication is available at Springer via http://dx.doi.org/10.1007/s00165-012-0244-5. Copyright © 2012, British Computer Society. | en_US |
dc.description.abstract | Formal methods are one of the most important approaches to increasing the confidence in the correctness of software systems. A formal specification can be used as an oracle in testing since one can determine whether an observed behaviour is allowed by the specification. This is an important feature of formal testing: behaviours of the system observed in testing are compared with the specification and ideally this comparison is automated. In this paper we study a formal testing framework to deal with systems that interact with their environment at physically distributed interfaces, called ports, and where choices between different possibilities are probabilistically quantified. Building on previous work, we introduce two families of schedulers to resolve nondeterministic choices among different actions of the system. The first type of schedulers, which we call global schedulers, resolves nondeterministic choices by representing the environment as a single global scheduler. The second type, which we call localised schedulers, models the environment as a set of schedulers with there being one scheduler for each port. We formally define the application of schedulers to systems and provide and study different implementation relations in this setting. | en_US |
dc.language.iso | en | en_US |
dc.publisher | Springer | en_US |
dc.subject | Distributed systems | en_US |
dc.subject | Formal testing | en_US |
dc.subject | Probabilistic systems | en_US |
dc.subject | Schedulers | en_US |
dc.title | Using schedulers to test probabilistic distributed systems | en_US |
dc.type | Article | en_US |
dc.identifier.doi | http://dx.doi.org/10.1007/s00165-012-0244-5 | - |
pubs.organisational-data | /Brunel | - |
pubs.organisational-data | /Brunel/Administration and Support Staff | - |
pubs.organisational-data | /Brunel/Administration and Support Staff/Administration and Support Staff | - |
pubs.organisational-data | /Brunel/Brunel Active Staff | - |
pubs.organisational-data | /Brunel/Brunel Active Staff/School of Info. Systems, Comp & Maths | - |
pubs.organisational-data | /Brunel/Brunel Active Staff/School of Info. Systems, Comp & Maths/Computer Science | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/Brunel Business School - URCs and Groups | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/Brunel Business School - URCs and Groups/Centre for Research into Entrepreneurship, International Business and Innovation in Emerging Markets | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Arts - URCs and Groups | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Arts - URCs and Groups/Brunel Centre for Contemporary Writing | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Health Sciences and Social Care - URCs and Groups | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Health Sciences and Social Care - URCs and Groups/Brunel Institute for Ageing Studies | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Health Sciences and Social Care - URCs and Groups/Brunel Institute of Cancer Genetics and Pharmacogenomics | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Health Sciences and Social Care - URCs and Groups/Centre for Systems and Synthetic Biology | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Information Systems, Computing and Mathematics - URCs and Groups | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Information Systems, Computing and Mathematics - URCs and Groups/Centre for Information and Knowledge Management | - |
pubs.organisational-data | /Brunel/University Research Centres and Groups/School of Information Systems, Computing and Mathematics - URCs and Groups/Multidisclipary Assessment of Technology Centre for Healthcare (MATCH) | - |
Appears in Collections: | Computer Science Dept of Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 283.81 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.