UPPAAL in Practice: Quantitative Verication of a RapidIO Network


Share/Save/Bookmark

Xing, Jiansheng and Theelen, Bart D. and Langerak, Rom and Pol van de, Jaco and Tretmans, Jan and Voeten, J.P.M. (2010) UPPAAL in Practice: Quantitative Verication of a RapidIO Network. In: 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010, 18-20 October 2010, Amirandes, Heraclion, Crete. (In Press)

[img]PDF
Restricted to UT campus only
: Request a copy
719Kb
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.
Item Type:Conference or Workshop Item
Copyright:© 2010 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/72602
Official URL:http://dx.doi.org/10.1007/978-3-642-16561-0_20
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 279111