UPPAAL in Practice: Quantitative Verication of a RapidIO Network


Xing, Jiansheng and Theelen, Bart D. and Langerak, Rom and Pol, Jaco van de 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 (pp. pp. 160-174). (In Press)

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


Repository Staff Only: item control page

Metis ID: 279111