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 proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
27 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 languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification, and Validation
Subtitle of host publication4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationBerlin
PublisherSpringer
Pages160-174
Number of pages15
ISBN (Electronic)978-3-642-16561-0
ISBN (Print)978-3-642-16560-3
DOIs
Publication statusPublished - 18 Oct 2010
Event4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 - Heraklion, Greece
Duration: 18 Oct 201021 Oct 2010
Conference number: 4
http://isola-conference.org/isola2010/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6416
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010
Abbreviated titleISoLA 2010
CountryGreece
CityHeraklion
Period18/10/1021/10/10
Internet address

Fingerprint

Packet networks
Object oriented programming
Model checking
Distributed computer systems
Motion control
Industry

Keywords

  • METIS-279111
  • IR-72602
  • 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
  • EWI-18262
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • quantitative verification

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). Berlin: Springer. https://doi.org/10.1007/978-3-642-16561-0_20
Xing, Jiansheng ; Theelen, Bart D. ; Langerak, Rom ; van de Pol, Jaco ; Tretmans, Jan ; Voeten, J.P.M. / 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 = "METIS-279111, IR-72602, 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, EWI-18262, 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",
note = "eemcs-eprint-18262",
year = "2010",
month = "10",
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",

}

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; van de Pol, Jaco ; Tretmans, Jan; Voeten, J.P.M.

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 proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - UPPAAL in Practice

T2 - Quantitative Verication of a RapidIO Network

AU - Xing, Jiansheng

AU - Theelen, Bart D.

AU - Langerak, Rom

AU - van de Pol, Jaco

AU - Tretmans, Jan

AU - Voeten, J.P.M.

N1 - eemcs-eprint-18262

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 - METIS-279111

KW - IR-72602

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 - EWI-18262

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

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). https://doi.org/10.1007/978-3-642-16561-0_20