A Scalable Incomplete Test for the Boundedness of UML RT Models

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:9f1f111f40d066a6fc4728f1a331b97c

LEUE, Stefan, Richard MAYR, Wei WEI, 2004. A Scalable Incomplete Test for the Boundedness of UML RT Models. In: JENSEN, Kurt, ed., Andreas PODELSKI, ed.. Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer Berlin Heidelberg, pp. 327-341. ISBN 978-3-540-21299-7. Available under: doi: 10.1007/978-3-540-24730-2_26

@inproceedings{Leue2004Scala-5567, title={A Scalable Incomplete Test for the Boundedness of UML RT Models}, year={2004}, doi={10.1007/978-3-540-24730-2_26}, number={2988}, isbn={978-3-540-21299-7}, address={Berlin, Heidelberg}, publisher={Springer Berlin Heidelberg}, series={Lecture Notes in Computer Science}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, pages={327--341}, editor={Jensen, Kurt and Podelski, Andreas}, author={Leue, Stefan and Mayr, Richard and Wei, Wei} }

Wei, Wei Leue, Stefan Wei, Wei application/pdf Mayr, Richard Mayr, Richard deposit-license 2011-03-24T15:56:29Z 2004 2011-03-24T15:56:29Z We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We reduce UML RT models to systems of communicating finite state machines (CFSMs). We propose a series of further abstractions that leaves us with a system of linear inequalities. Those represent the message sending and receiving effect that the control flow cycles of every process have on the overall message buffer. The test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. We discuss the complexity of this test and present experimental results using the IBOC system that we are implementing. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flow graphs that are derived from UML RT models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models.We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. While we focus on the analysis of UML RT models, the analysis<br />can directly be applied to any type of CFSM models. A Scalable Incomplete Test for the Boundedness of UML RT Models First publ. in: Lecture notes in computer science, No. 2988 (2004), pp. 327-341 eng Leue, Stefan

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

A_Scalable_Incomplete_Test_for_the_Boundedness_of_UML_RT_Models.pdf 95

Das Dokument erscheint in:

deposit-license Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: deposit-license

KOPS Suche


Stöbern

Mein Benutzerkonto