World Scientific
  • Search
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×
Our website is made possible by displaying certain online content using javascript.
In order to view the full content, please disable your ad blocker or whitelist our website www.worldscientific.com.

System Upgrade on Tue, Oct 25th, 2022 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

Multi-core and multi-processor architectures have predominated the domain of embedded systems permitting easy mapping of concurrent applications to such architectures. The programs, in general, are subjected to significant optimizing and parallelizing transformations, automated and also human guided, before being mapped to an architecture. Modelling parallel behaviour and formally verifying that their functionality is preserved during synthesis are challenging tasks. Untimed PRES+ models are found to be suitable for the specification of parallel behaviour. Path cover oriented equivalence checking methods have been found to be quite effective for sequential behaviour. Path construction for parallel behaviour, however, is significantly more complex than that for sequential behaviour due to all possible interleavings of the parallel operations. Identification of the path covers depends upon choosing appropriate cut-points. In this paper, the need for introducing cut-points dynamically has been underlined and a mechanism to achieve this task is proposed. Details on how to construct a path cover using dynamic cut-points is presented.

Communicated by S.D. Bruda