DOI: https://doi.org/10.5815/ijem.2011.01.11, Pub. Date: 8 Feb. 2011
For verification of component behavior compatibility in component-based real-time system, we make use of the timed automata to formally describe the component. In this way, the problem of component behavior compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system’s TA models. We then use the verification function of UPPAAL to automatically generate result, and finally conduct a case study to demonstrate how our technique works.
[...] Read more.
