Sciweavers

Share
TACAS
2004
Springer

A Scalable Incomplete Test for the Boundedness of UML RT Models

10 years 5 months ago
A Scalable Incomplete Test for the Boundedness of UML RT Models
Abstract. 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 (CFpropose 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....
Stefan Leue, Richard Mayr, Wei Wei
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where TACAS
Authors Stefan Leue, Richard Mayr, Wei Wei
Comments (0)
books