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 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/Territory | Greece |
City | Heraklion |
Period | 18/10/10 → 21/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