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

    4 Citations (Scopus)
    52 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

    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

    Fingerprint Dive into the research topics of 'UPPAAL in Practice: Quantitative Verication of a RapidIO Network'. Together they form a unique fingerprint.

  • 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