Untanglings: a novel approach to analyzing concurrent systems

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)
ID: 605516308
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