UPPAAL in Practice: Quantitative Verication of a RapidIO Network

Jiansheng Xing; Bart D. Theelen; Rom Langerak; Jaco  van de Pol; Jan Tretmans; J.P.M. Voeten

doi:10.1007/978-3-642-16561-0_20

UPPAAL in Practice: Quantitative Verication of a RapidIO Network

Jiansheng Xing, Bart D. Theelen, Rom Langerak, Jaco van de Pol, Jan Tretmans, J.P.M. Voeten

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

173 Downloads (Pure)

Abstract

Packet switched networks are widely used for interconnecting distributed computing platforms. RapidIO (Rapid Input/Output) is an industry standard for packet switched networks to interconnect multiple processor boards. Key performance metrics for these platforms include average-case and worst-case packet transfer latencies. We focus on verifying such quantitative properties for a RapidIO based multi-processor platform that executes a motion control application. A performance model is available in the Parallel Object-Oriented Specication Language (POOSL) that allows for simulation based estimation results. It is however required to determine the exact worst-case latency as the application is time-critical. A model checking approach has been proposed in our previous work which transforms the POOSL model into an UPPAAL model. However, such an approach only works for a fairly small system. We extend the transformation approach with various heuristics to reduce the underlying state space, thereby providing an eective approximation approach that scales to industrial problems of a reasonable complexity.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification, and Validation
Subtitle of host publication	4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II
Editors	Tiziana Margaria, Bernhard Steffen
Place of Publication	Berlin
Publisher	Springer
Pages	160-174
Number of pages	15
ISBN (Electronic)	978-3-642-16561-0
ISBN (Print)	978-3-642-16560-3
DOIs	https://doi.org/10.1007/978-3-642-16561-0_20
Publication status	Published - 18 Oct 2010
Event	4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 - Heraklion, Greece Duration: 18 Oct 2010 → 21 Oct 2010 Conference number: 4 http://isola-conference.org/isola2010/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	6416
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010
Abbreviated title	ISoLA 2010
Country/Territory	Greece
City	Heraklion
Period	18/10/10 → 21/10/10
Internet address	http://isola-conference.org/isola2010/

Keywords

UPPAAL
Transformation
Heuristic
FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
POOSL
EC Grant Agreement nr.: FP7/214755
EC Grant Agreement nr.: FP7-ICT-2007-1
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
quantitative verification

Access to Document

10.1007/978-3-642-16561-0_20

UPPAAL in PracticeAccepted author version, 719 KB

Cite this

Xing, J., Theelen, B. D., Langerak, R., van de Pol, J., Tretmans, J., & Voeten, J. P. M. (2010). UPPAAL in Practice: Quantitative Verication of a RapidIO Network. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II (pp. 160-174). (Lecture Notes in Computer Science; Vol. 6416). Springer. https://doi.org/10.1007/978-3-642-16561-0_20

Xing, Jiansheng ; Theelen, Bart D. ; Langerak, Rom et al. / UPPAAL in Practice : Quantitative Verication of a RapidIO Network. Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. editor / Tiziana Margaria ; Bernhard Steffen. Berlin : Springer, 2010. pp. 160-174 (Lecture Notes in Computer Science).

@inproceedings{ace02c8e676b45a8a4080b3049965d0b,

title = "UPPAAL in Practice: Quantitative Verication of a RapidIO Network",

abstract = "Packet switched networks are widely used for interconnecting distributed computing platforms. RapidIO (Rapid Input/Output) is an industry standard for packet switched networks to interconnect multiple processor boards. Key performance metrics for these platforms include average-case and worst-case packet transfer latencies. We focus on verifying such quantitative properties for a RapidIO based multi-processor platform that executes a motion control application. A performance model is available in the Parallel Object-Oriented Specication Language (POOSL) that allows for simulation based estimation results. It is however required to determine the exact worst-case latency as the application is time-critical. A model checking approach has been proposed in our previous work which transforms the POOSL model into an UPPAAL model. However, such an approach only works for a fairly small system. We extend the transformation approach with various heuristics to reduce the underlying state space, thereby providing an eective approximation approach that scales to industrial problems of a reasonable complexity.",

keywords = "UPPAAL, Transformation, Heuristic, FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS, POOSL, EC Grant Agreement nr.: FP7/214755, EC Grant Agreement nr.: FP7-ICT-2007-1, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, quantitative verification",

author = "Jiansheng Xing and Theelen, {Bart D.} and Rom Langerak and {van de Pol}, Jaco and Jan Tretmans and J.P.M. Voeten",

year = "2010",

month = oct,

day = "18",

doi = "10.1007/978-3-642-16561-0_20",

language = "English",

isbn = "978-3-642-16560-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "160--174",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification, and Validation",

address = "Netherlands",

note = "4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010, ISoLA 2010 ; Conference date: 18-10-2010 Through 21-10-2010",

url = "http://isola-conference.org/isola2010/",

}

Xing, J, Theelen, BD, Langerak, R , van de Pol, J, Tretmans, J & Voeten, JPM 2010, UPPAAL in Practice: Quantitative Verication of a RapidIO Network. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Lecture Notes in Computer Science, vol. 6416, Springer, Berlin, pp. 160-174, 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010, Heraklion, Greece, 18/10/10. https://doi.org/10.1007/978-3-642-16561-0_20

UPPAAL in Practice : Quantitative Verication of a RapidIO Network. / Xing, Jiansheng; Theelen, Bart D.; Langerak, Rom et al.

Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. ed. / Tiziana Margaria; Bernhard Steffen. Berlin : Springer, 2010. p. 160-174 (Lecture Notes in Computer Science; Vol. 6416).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - UPPAAL in Practice

T2 - 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010

AU - Xing, Jiansheng

AU - Theelen, Bart D.

AU - Langerak, Rom

AU - van de Pol, Jaco

AU - Tretmans, Jan

AU - Voeten, J.P.M.

N1 - Conference code: 4

PY - 2010/10/18

Y1 - 2010/10/18

N2 - Packet switched networks are widely used for interconnecting distributed computing platforms. RapidIO (Rapid Input/Output) is an industry standard for packet switched networks to interconnect multiple processor boards. Key performance metrics for these platforms include average-case and worst-case packet transfer latencies. We focus on verifying such quantitative properties for a RapidIO based multi-processor platform that executes a motion control application. A performance model is available in the Parallel Object-Oriented Specication Language (POOSL) that allows for simulation based estimation results. It is however required to determine the exact worst-case latency as the application is time-critical. A model checking approach has been proposed in our previous work which transforms the POOSL model into an UPPAAL model. However, such an approach only works for a fairly small system. We extend the transformation approach with various heuristics to reduce the underlying state space, thereby providing an eective approximation approach that scales to industrial problems of a reasonable complexity.

AB - Packet switched networks are widely used for interconnecting distributed computing platforms. RapidIO (Rapid Input/Output) is an industry standard for packet switched networks to interconnect multiple processor boards. Key performance metrics for these platforms include average-case and worst-case packet transfer latencies. We focus on verifying such quantitative properties for a RapidIO based multi-processor platform that executes a motion control application. A performance model is available in the Parallel Object-Oriented Specication Language (POOSL) that allows for simulation based estimation results. It is however required to determine the exact worst-case latency as the application is time-critical. A model checking approach has been proposed in our previous work which transforms the POOSL model into an UPPAAL model. However, such an approach only works for a fairly small system. We extend the transformation approach with various heuristics to reduce the underlying state space, thereby providing an eective approximation approach that scales to industrial problems of a reasonable complexity.

KW - UPPAAL

KW - Transformation

KW - Heuristic

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

KW - POOSL

KW - EC Grant Agreement nr.: FP7/214755

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - quantitative verification

U2 - 10.1007/978-3-642-16561-0_20

DO - 10.1007/978-3-642-16561-0_20

M3 - Conference contribution

SN - 978-3-642-16560-3

T3 - Lecture Notes in Computer Science

SP - 160

EP - 174

BT - Leveraging Applications of Formal Methods, Verification, and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

CY - Berlin

Y2 - 18 October 2010 through 21 October 2010

ER -

Xing J, Theelen BD, Langerak R , van de Pol J, Tretmans J, Voeten JPM. UPPAAL in Practice: Quantitative Verication of a RapidIO Network. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Berlin: Springer. 2010. p. 160-174. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-16561-0_20

UPPAAL in Practice: Quantitative Verication of a RapidIO Network

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this