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)
    38 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

    • 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

    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 = "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 = "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.

    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

    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