Guaranteeing Resource Bounds for Component Software

Component software is software that has been assembled from various pieces of standardized, reusable computer programs, so-called components. Executing component software creates instances of these components. For several reasons, for example, limited resources and/or application requirements, it can be important to have control over the number of such instances. In our previous work, we have given an abstract component language and a type system which ensures that the number of simultaneously active instances of any component never exceeds a sharp bound expressed in the type. The language featured instantiation and reuse of components, as well as sequential composition, choice and scope. This work extends the previous one to include a parallel composition. Moreover, we improve on the operational semantics by using a small-step reduction relation. As a result, we can prove the soundness property of our static type system using the technique of Wright and Felleisen