Abstract
| Original language | English |
|---|---|
| Title of host publication | Leveraging Applications of Formal Methods, Verification, and Validation |
| Subtitle of host publication | 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II |
| Editors | Tiziana Margaria, Bernhard Steffen |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 160-174 |
| Number of pages | 15 |
| ISBN (Electronic) | 978-3-642-16561-0 |
| ISBN (Print) | 978-3-642-16560-3 |
| DOIs | |
| Publication status | Published - 18 Oct 2010 |
| Event | 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 - Heraklion, Greece Duration: 18 Oct 2010 → 21 Oct 2010 Conference number: 4 http://isola-conference.org/isola2010/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 6416 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 |
|---|---|
| Abbreviated title | ISoLA 2010 |
| Country | Greece |
| City | Heraklion |
| Period | 18/10/10 → 21/10/10 |
| Internet address |
Fingerprint
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
}
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 proceeding › Conference contribution › Academic › peer-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 -