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

doi:10.1109/ACSD.2010.21

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 proceeding › Conference contribution › Academic › peer-review

9 Citations (Scopus)

111 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 language	English
Title of host publication	10 International Conference on Application of Concurrency to System Design
Subtitle of host publication	proceedings : 21-25 June 2010, Braga, Portugal
Editors	L. Gomes, V. Khomenko, J.M. Fernandes
Place of Publication	Los Alamitos, CA
Publisher	IEEE
Pages	47-56
Number of pages	10
ISBN (Print)	978-0-7695-4066-5
DOIs	https://doi.org/10.1109/ACSD.2010.21
Publication status	Published - Jun 2010
Event	10th International Conference on Application of Concurrency to System Design, ACSD 2010 - Braga, Portugal Duration: 21 Jun 2010 → 25 Jun 2010 Conference number: 10

Publication series

Name	International Conference on Application of Concurrency to System Design
Publisher	IEEE Computer Society Press
Volume	2010
ISSN (Print)	1550-4808

Conference

Conference	10th International Conference on Application of Concurrency to System Design, ACSD 2010
Abbreviated title	ACSD
Country/Territory	Portugal
City	Braga
Period	21/06/10 → 25/06/10

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

Access to Document

10.1109/ACSD.2010.21

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). IEEE. https://doi.org/10.1109/ACSD.2010.21

Xing, Jiansheng ; Theelen, B.D. ; Langerak, Rom et al. / 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, 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 = jun,

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",

pages = "47--56",

editor = "L. Gomes and V. Khomenko and J.M. Fernandes",

booktitle = "10 International Conference on Application of Concurrency to System Design",

address = "United States",

note = "10th International Conference on Application of Concurrency to System Design, ACSD 2010, ACSD ; Conference date: 21-06-2010 Through 25-06-2010",

}

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, 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 et al.
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, 2010. p. 47-56 (International Conference on Application of Concurrency to System Design; Vol. 2010).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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.

N1 - Conference code: 10

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

CY - Los Alamitos, CA

T2 - 10th International Conference on Application of Concurrency to System Design, ACSD 2010

Y2 - 21 June 2010 through 25 June 2010

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. 2010. p. 47-56. (International Conference on Application of Concurrency to System Design). doi: 10.1109/ACSD.2010.21

From POOSL to UPPAAL: Transformation and Quantitative Analysis

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this