Paper Info
Title
From POOSL to UPPAAL: Transformation and Quantitative Analysis
Abstract
POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.
Year
DOI
Venue
2010
10.1109/ACSD.2010.21
ACSD
Keywords
Field
DocType
transformation analysis,average-case latency,exact worst-case latency,poosl analysis,considered motion control algorithm,motion control,parallel programming,worst-case latency,model checking tool uppaal,parallel object oriented specification language,motion control system,verification,transformation,model checking technique,uppaal model,uppaal,poosl,quantitative analysis,motion control systems,poosl model,rapidio packet swiches,object-oriented languages,performance,periodic execution,power generation,object oriented languages,input output,modeling language,model checking,automata,switches,synchronization
Specification language,Motion control,Synchronization,Model checking,Computer science,Network packet,Modeling language,Real-time computing,Theoretical computer science,RapidIO,Design space exploration
Conference
ISSN
ISBN
Citations 
1550-4808 E-ISBN : 978-1-4244-7267-3
978-1-4244-7267-3
4
PageRank 
References 
Authors
0.45
7
6
Name
Order
Citations
PageRank
Jiansheng Xing1141.32
B. D. Theelen225412.80
Rom Langerak330839.16
Jaco Van De Pol4102278.19
Jan Tretmans5162497.10
J. P. M. Voeten6806.82