UPPAAL in Practice: Quantitative Verication of a RapidIO Network

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)

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 279111