Traditional type systems specify interfaces in terms of values and domains. A function f: Z -> R expects integers and promises to produce a real number. When we apply a function to an argument, or when we compose two functions, we have to check that their types match. This talk will present time and resource interfaces, which extend type systems with the ability to reason about the dynamic behavior of software components. Like type systems, interfaces specify the input assumptions a component makes on its environment and the output guarantees it provides. For instance, one can specify the temporal order in which method calls to a component should occur, deadlines for providing input to this component, or the resources it needs to work correctly. In return, the component provides certain output guarantees, such as in-time delivery of its service, bounds on its resource consumption, etc. Technically, interfaces are games in which the system plays against the environment. Game theoretic algorithms allow us to check if two components are compatible (i.e. if there exists an environment in which all input assumptions are met) and to synthesize the composite interface.
(joint work with Luca de Alfaro, Tom Henzinger and Arindam Chakrabarti)
| rupak@cs.ucla.edu | Last updated: May 23, 2005 |