Untanglings: a novel approach to analyzing concurrent systems
Gespeichert in:
Verfasser / Beitragende:
[Artem Polyvyanyy, Marcello La Rosa, Chun Ouyang, Arthur ter Hofstede]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/5-6(2015-11-01), 753-788
Format:
Artikel (online)
Online Zugang:
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516308 | ||
| 003 | CHVBK | ||
| 005 | 20210128100713.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20151101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0329-4 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0329-4 | ||
| 245 | 0 | 0 | |a Untanglings: a novel approach to analyzing concurrent systems |h [Elektronische Daten] |c [Artem Polyvyanyy, Marcello La Rosa, Chun Ouyang, Arthur ter Hofstede] |
| 520 | 3 | |a Substantial research efforts have been expended to deal with the complexity of concurrent systems that is inherent to their analysis, e.g., works that tackle the well-known state space explosion problem. Approaches differ in the classes of properties that they are able to suitably check and this is largely a result of the way they balance the trade-off between analysis time and space employed to describe a concurrent system. One interesting class of properties is concerned with behavioral characteristics. These properties are conveniently expressed in terms of computations, or runs, in concurrent systems. This article introduces the theory of untanglings that exploits a particular representation of a collection of runs in a concurrent system. It is shown that a representative untangling of a bounded concurrent system can be constructed that captures all and only the behavior of the system. Representative untanglings strike a unique balance between time and space, yet provide a single model for the convenient extraction of various behavioral properties. Performance measurements in terms of construction time and size of representative untanglings with respect to the original specifications of concurrent systems, conducted on a collection of models from practice, confirm the scalability of the approach. Finally, this article demonstrates practical benefits of using representative untanglings when checking various behavioral properties of concurrent systems. | |
| 540 | |a British Computer Society, 2015 | ||
| 690 | 7 | |a Concurrency |2 nationallicence | |
| 690 | 7 | |a Concurrent systems |2 nationallicence | |
| 690 | 7 | |a Analysis |2 nationallicence | |
| 690 | 7 | |a Untanglings |2 nationallicence | |
| 690 | 7 | |a Representative untanglings |2 nationallicence | |
| 700 | 1 | |a Polyvyanyy |D Artem |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | |
| 700 | 1 | |a La Rosa |D Marcello |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | |
| 700 | 1 | |a Ouyang |D Chun |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | |
| 700 | 1 | |a ter Hofstede |D Arthur |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 753-788 |x 0934-5043 |q 27:5-6<753 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0329-4 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0329-4 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Polyvyanyy |D Artem |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a La Rosa |D Marcello |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Ouyang |D Chun |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a ter Hofstede |D Arthur |u Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 753-788 |x 0934-5043 |q 27:5-6<753 |1 2015 |2 27 |o 165 | ||