Title
UPPAAL in practice: quantitative verification of a RapidIO network
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 multiprocessor 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.
Year
DOI
Venue
2010
10.1007/978-3-642-16561-0_20
ISoLA
Keywords
Field
DocType
quantitative verification,model checking approach,key performance metrics,effective approximation approach,rapidio network,worst-case packet transfer latency,uppaal model,exact worst-case latency,transformation approach,performance model,motion control application,poosl model,state space,motion control,distributed computing,model checking,input output
Specification language,Heuristic,Model checking,Computer science,Network packet,RapidIO,Multiprocessing,Heuristics,State space,Distributed computing
Conference
Volume
ISSN
ISBN
6416
0302-9743
3-642-16560-5
Citations 
PageRank 
References 
1
0.35
6
Authors
6
Name
Order
Citations
PageRank
Jiansheng Xing1141.32
Bart Theelen218410.89
Rom Langerak330839.16
Jaco Van De Pol4102278.19
Jan Tretmans5162497.10
J. P. M. Voeten6806.82