From POOSL to UPPAAL: Transformation and Quantitative Analysis

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)
    85 Downloads (Pure)

    Abstract

    POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.
    Original languageEnglish
    Title of host publication10 International Conference on Application of Concurrency to System Design
    Subtitle of host publicationproceedings : 21-25 June 2010, Braga, Portugal
    EditorsL. Gomes, V. Khomenko, J.M. Fernandes
    Place of PublicationLos Alamitos, CA
    PublisherIEEE Computer Society Press
    Pages47-56
    Number of pages10
    ISBN (Print)978-0-7695-4066-5
    DOIs
    Publication statusPublished - Jun 2010
    Event10th International Conference on Application of Concurrency to System Design, ACSD 2010 - Braga, Portugal
    Duration: 21 Jun 201025 Jun 2010
    Conference number: 10

    Publication series

    NameInternational Conference on Application of Concurrency to System Design
    PublisherIEEE Computer Society Press
    Volume2010
    ISSN (Print)1550-4808

    Conference

    Conference10th International Conference on Application of Concurrency to System Design, ACSD 2010
    Abbreviated titleACSD
    CountryPortugal
    CityBraga
    Period21/06/1025/06/10

    Fingerprint

    Specification languages
    Motion control
    Control systems
    Chemical analysis
    Model checking
    Switches

    Keywords

    • POOSL
    • Verification
    • Quantitative analysis
    • UPPAAL
    • EC Grant Agreement nr.: FP7/214755
    • EC Grant Agreement nr.: FP7-ICT-2007-1
    • Performance
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • CR-B.2.2
    • CR-B.8
    • Transformation

    Cite this

    Xing, J., Theelen, B. D., Langerak, R., van de Pol, J., Tretmans, J., & Voeten, J. P. M. (2010). From POOSL to UPPAAL: Transformation and Quantitative Analysis. In L. Gomes, V. Khomenko, & J. M. Fernandes (Eds.), 10 International Conference on Application of Concurrency to System Design: proceedings : 21-25 June 2010, Braga, Portugal (pp. 47-56). (International Conference on Application of Concurrency to System Design; Vol. 2010). Los Alamitos, CA: IEEE Computer Society Press. https://doi.org/10.1109/ACSD.2010.21
    Xing, Jiansheng ; Theelen, B.D. ; Langerak, Rom ; van de Pol, Jaco ; Tretmans, Jan ; Voeten, J.P.M. / From POOSL to UPPAAL: Transformation and Quantitative Analysis. 10 International Conference on Application of Concurrency to System Design: proceedings : 21-25 June 2010, Braga, Portugal. editor / L. Gomes ; V. Khomenko ; J.M. Fernandes. Los Alamitos, CA : IEEE Computer Society Press, 2010. pp. 47-56 (International Conference on Application of Concurrency to System Design).
    @inproceedings{8f862e29ff4d41f0a9f8a121c35a0b2a,
    title = "From POOSL to UPPAAL: Transformation and Quantitative Analysis",
    abstract = "POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.",
    keywords = "POOSL, Verification, Quantitative analysis, UPPAAL, EC Grant Agreement nr.: FP7/214755, EC Grant Agreement nr.: FP7-ICT-2007-1, Performance, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, CR-B.2.2, CR-B.8, Transformation",
    author = "Jiansheng Xing and B.D. Theelen and Rom Langerak and {van de Pol}, Jaco and Jan Tretmans and J.P.M. Voeten",
    year = "2010",
    month = "6",
    doi = "10.1109/ACSD.2010.21",
    language = "English",
    isbn = "978-0-7695-4066-5",
    series = "International Conference on Application of Concurrency to System Design",
    publisher = "IEEE Computer Society Press",
    pages = "47--56",
    editor = "L. Gomes and V. Khomenko and J.M. Fernandes",
    booktitle = "10 International Conference on Application of Concurrency to System Design",

    }

    Xing, J, Theelen, BD, Langerak, R, van de Pol, J, Tretmans, J & Voeten, JPM 2010, From POOSL to UPPAAL: Transformation and Quantitative Analysis. in L Gomes, V Khomenko & JM Fernandes (eds), 10 International Conference on Application of Concurrency to System Design: proceedings : 21-25 June 2010, Braga, Portugal. International Conference on Application of Concurrency to System Design, vol. 2010, IEEE Computer Society Press, Los Alamitos, CA, pp. 47-56, 10th International Conference on Application of Concurrency to System Design, ACSD 2010, Braga, Portugal, 21/06/10. https://doi.org/10.1109/ACSD.2010.21

    From POOSL to UPPAAL: Transformation and Quantitative Analysis. / Xing, Jiansheng; Theelen, B.D.; Langerak, Rom; van de Pol, Jaco; Tretmans, Jan; Voeten, J.P.M.

    10 International Conference on Application of Concurrency to System Design: proceedings : 21-25 June 2010, Braga, Portugal. ed. / L. Gomes; V. Khomenko; J.M. Fernandes. Los Alamitos, CA : IEEE Computer Society Press, 2010. p. 47-56 (International Conference on Application of Concurrency to System Design; Vol. 2010).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - From POOSL to UPPAAL: Transformation and Quantitative Analysis

    AU - Xing, Jiansheng

    AU - Theelen, B.D.

    AU - Langerak, Rom

    AU - van de Pol, Jaco

    AU - Tretmans, Jan

    AU - Voeten, J.P.M.

    PY - 2010/6

    Y1 - 2010/6

    N2 - POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.

    AB - POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.

    KW - POOSL

    KW - Verification

    KW - Quantitative analysis

    KW - UPPAAL

    KW - EC Grant Agreement nr.: FP7/214755

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

    KW - Performance

    KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    KW - CR-B.2.2

    KW - CR-B.8

    KW - Transformation

    U2 - 10.1109/ACSD.2010.21

    DO - 10.1109/ACSD.2010.21

    M3 - Conference contribution

    SN - 978-0-7695-4066-5

    T3 - International Conference on Application of Concurrency to System Design

    SP - 47

    EP - 56

    BT - 10 International Conference on Application of Concurrency to System Design

    A2 - Gomes, L.

    A2 - Khomenko, V.

    A2 - Fernandes, J.M.

    PB - IEEE Computer Society Press

    CY - Los Alamitos, CA

    ER -

    Xing J, Theelen BD, Langerak R, van de Pol J, Tretmans J, Voeten JPM. From POOSL to UPPAAL: Transformation and Quantitative Analysis. In Gomes L, Khomenko V, Fernandes JM, editors, 10 International Conference on Application of Concurrency to System Design: proceedings : 21-25 June 2010, Braga, Portugal. Los Alamitos, CA: IEEE Computer Society Press. 2010. p. 47-56. (International Conference on Application of Concurrency to System Design). https://doi.org/10.1109/ACSD.2010.21