Application specific digital systems, called embedded systems, touch almost every aspect of modern human life. As a result, there is considerable interest in automating the design (called synthesis) of these systems. Further, given the time-to-market pressures and increasing system complexities, component reuse during synthesis is being touted as a key to success. This thesis proposes a formal framework for reusing system-level components during synthesis. Within the framework for component reuse, component matching is a key problem that must be addressed. Given the specification of a design function, and a device stored as a component in a library, component matching addresses the question of whether the device can implement the function. Often system-level components are multi-functional and generic, and it is rarely the case that the function is directly realizable by a device. Hence, an important aspect of matching is to decide whether the device can be dynamically adapted to match the function. This thesis proposes a formalization of the matching problem using formal models of the function and device, denoted by F and D respectively. D matches F provided there exists an interface I that adapts D dynamically to produce the same behaviour as F. None of the existing implementation verification techniques within formal methods can be used to test for the existence of an I between arbitrary pairs of F and D. In this thesis, a new simulation relation called forced simulation is proposed between the states of F and D. It is then formally established that the existence of a forced simulation relation is a necessary and sufficient condition for the existence of I for a pair of F and d. Two kinds of forced simulation are proposed, one each for synchronous and asynchronous interactions with the environment. Based on forced simulation, a polynomial time algorithm for automatic matching of F and D is also developed. The distinguishing feature of the algorithm is that when successful, it generates an interface that automatically adapts the device to behave like the function. The algorithm is illustrated by reusing two rogrammable components from Intel and some typical embedded controllers.
| Identifer | oai:union.ndltd.org:ADTP/187879 |
| Date | January 2000 |
| Creators | Roop, Parthasarathi, Computer Science & Engineering, Faculty of Engineering, UNSW |
| Publisher | Awarded by:University of New South Wales. School of Computer Science and Engineering |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Rights | Copyright Parthasarathi Roop, http://unsworks.unsw.edu.au/copyright |
Page generated in 0.0021 seconds