The Paths to Choreography Extraction

Luís Cruz-Filipe; Kim S. Larsen; Fabrizio Montesi

doi:10.1007/978-3-662-54458-7_25

The Paths to Choreography Extraction

Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

131 Downloads (Pure)

Abstract

Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.

We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures : Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Editors	Javier Esparza, Andrzej S. Murawski
Publisher	Springer
Publication date	2017
Pages	424-440
ISBN (Print)	978-3-662-54457-0
ISBN (Electronic)	978-3-662-54458-7
DOIs	https://doi.org/10.1007/978-3-662-54458-7_25
Publication status	Published - 2017
Event	20th International Conference on Foundations of Software Science and Computation Structures - Uppsala, Sweden Duration: 22. Apr 2017 → 29. Apr 2017 Conference number: 20

Conference

Conference	20th International Conference on Foundations of Software Science and Computation Structures
Number	20
Country/Territory	Sweden
City	Uppsala
Period	22/04/2017 → 29/04/2017

Series	Lecture Notes in Computer Science
Volume	10203
ISSN	0302-9743

Documents & Links

10.1007/978-3-662-54458-7_25

The Paths to Choreography ExtractionSubmitted manuscript, 256 KB

https://arxiv.org/pdf/1610.10050.pdf

Cite this

Cruz-Filipe, L., Larsen, K. S., & Montesi, F. (2017). The Paths to Choreography Extraction. In J. Esparza, & A. S. Murawski (Eds.), Foundations of Software Science and Computation Structures: Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 (pp. 424-440). Springer. Lecture Notes in Computer Science Vol. 10203 https://doi.org/10.1007/978-3-662-54458-7_25

Cruz-Filipe, Luís ; Larsen, Kim S. ; Montesi, Fabrizio. / The Paths to Choreography Extraction. Foundations of Software Science and Computation Structures: Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. editor / Javier Esparza ; Andrzej S. Murawski. Springer, 2017. pp. 424-440 (Lecture Notes in Computer Science, Vol. 10203).

@inproceedings{097341b575784aedaa0bdc9c32b111aa,

title = "The Paths to Choreography Extraction",

abstract = "Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.",

author = "Lu{\'i}s Cruz-Filipe and Larsen, {Kim S.} and Fabrizio Montesi",

year = "2017",

doi = "10.1007/978-3-662-54458-7_25",

language = "English",

isbn = "978-3-662-54457-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "424--440",

editor = "Javier Esparza and Murawski, {Andrzej S.}",

booktitle = "Foundations of Software Science and Computation Structures",

address = "Germany",

note = "20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 ; Conference date: 22-04-2017 Through 29-04-2017",

}

Cruz-Filipe, L , Larsen, KS & Montesi, F 2017, The Paths to Choreography Extraction. in J Esparza & AS Murawski (eds), Foundations of Software Science and Computation Structures: Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. Springer, Lecture Notes in Computer Science, vol. 10203, pp. 424-440, 20th International Conference on Foundations of Software Science and Computation Structures, Uppsala, Sweden, 22/04/2017. https://doi.org/10.1007/978-3-662-54458-7_25

The Paths to Choreography Extraction. / Cruz-Filipe, Luís ; Larsen, Kim S.; Montesi, Fabrizio.

Foundations of Software Science and Computation Structures: Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. ed. / Javier Esparza; Andrzej S. Murawski. Springer, 2017. p. 424-440 (Lecture Notes in Computer Science, Vol. 10203).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - The Paths to Choreography Extraction

AU - Cruz-Filipe, Luís

AU - Larsen, Kim S.

AU - Montesi, Fabrizio

N1 - Conference code: 20

PY - 2017

Y1 - 2017

N2 - Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.

AB - Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.

U2 - 10.1007/978-3-662-54458-7_25

DO - 10.1007/978-3-662-54458-7_25

M3 - Article in proceedings

SN - 978-3-662-54457-0

T3 - Lecture Notes in Computer Science

SP - 424

EP - 440

BT - Foundations of Software Science and Computation Structures

A2 - Esparza, Javier

A2 - Murawski, Andrzej S.

PB - Springer

T2 - 20th International Conference on Foundations of Software Science and Computation Structures

Y2 - 22 April 2017 through 29 April 2017

ER -

Cruz-Filipe L , Larsen KS , Montesi F. The Paths to Choreography Extraction. In Esparza J, Murawski AS, editors, Foundations of Software Science and Computation Structures: Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. Springer. 2017. p. 424-440. (Lecture Notes in Computer Science, Vol. 10203). doi: 10.1007/978-3-662-54458-7_25

The Paths to Choreography Extraction

Abstract

Conference

Documents & Links

Fingerprint

Cite this