UPPAAL in practice : quantitative verification of a RapidIO network.

J. Xing, B.D. Theelen, R. Langerak, J.C. Pol, van de, J. Tretmans, J.P.M. Voeten

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

4 Citaten (Scopus)
109 Downloads (Pure)

Samenvatting

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 Specification 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 effective approximation approach that scales to industrial problems of a reasonable complexity.
Originele taal-2Engels
TitelProceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010, October 18-21, 2010, Heraklion, Greece
RedacteurenT. Margaria, B. Steffen
Plaats van productieBerlin
UitgeverijSpringer
Pagina's160-174
ISBN van geprinte versie978-3-642-16561-0
DOI's
StatusGepubliceerd - 2010

Vingerafdruk Duik in de onderzoeksthema's van 'UPPAAL in practice : quantitative verification of a RapidIO network.'. Samen vormen ze een unieke vingerafdruk.

Citeer dit