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 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.
This work has been supported by the EU FP7 under grant number ICT-214755: Quasimodo.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Behrmann, G., David, R., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
van Bokhoven, L.: Constructive Tool Design for Formal Languages: From Semantics to Executing Models. Ph.D. thesis, Eindhoven University of Technology (2002)
Geilen, M.: Formal Techniques for Verification of Complex Real-Time Systems. Ph.D. thesis, Eindhoven University of Technology (2002)
Logothetis, G., Schneider, K.: Symbolic model checking of real-time systems. In: International Syposium on Temporal Representation and Reasoning, p. 214 (2001)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
van der Putten, P., Voeten, J.: Specification of Reactive Hardware/Software Systems. Ph.D. thesis, Eindhoven University of Technology (1997)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Shippen, G.: A technical overview of RapidIO. (November 2007), http://www.eetasia.com/ART_8800487921_499491_NP_7644b706.HTM
Theelen, B.D., Florescu, O., Geilen, M., Huang, J., van der Putten, P., Voeten, J.: Software/hardware engineering with the Parallel Object-Oriented Specification Language. In: MEMOCODE 2007: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, pp. 139–148. IEEE Computer Society, Washington (2007)
Xing, J., Theelen, B.D., Langerak, R., van de Pol, J., Tretmans, J., Voeten, J.: From POOSL to UPPAAL: Transformation and quantitative analysis. In: Proceedings of the International Conference on Application of Concurrency to System Design, pp. 47–56. IEEE Computer Society, Los Alamitos (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xing, J., Theelen, B.D., Langerak, R., van de Pol, J., Tretmans, J., Voeten, J.P.M. (2010). UPPAAL in Practice: Quantitative Verification of a RapidIO Network. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16561-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-16561-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16560-3
Online ISBN: 978-3-642-16561-0
eBook Packages: Computer ScienceComputer Science (R0)