This report presents our work on behavioral types for OSGi component systems. It extends previously published work and presents features and details that have not yet been published. In particular, we cover a discussion on behavioral types in general, and Eclipse based implementation work on behavioral types . The implementation work covers: editors, means for comparing types at development and runtime, a tool connection to resolve incompatibilities, and an AspectJ based infrastructure to ensure behavioral type correctness at runtime of a system. Furthermore, the implementation comprises various auxiliary operations. We present some evaluation work based on examples.
Our behavioral types represent an abstract view on the semantics of OSGi. We have summarized our work on the OSGi semantics in a report @cite_12 . Other work does describe OSGi and its semantics only at a very high level. A specification based on process algebras is featured in @cite_15 . Means for ensuring OSGi compatibility of bundles realized by using an advanced versioning system for OSGi bundles based on their type information is studied in @cite_31 . Some investigations on the relation between OSGi and some more formal component models have been done in @cite_27 . Aspects on formal security models for OSGi have been studied in @cite_25 .
@cite_31 @cite_27 @cite_15 @cite_25 @cite_12
1480723928 2110138217 126473541 1963705166
We present a formalization of the OSGi component framework. Our formalization is intended to be used as a basis for describing behavior of OSGi based systems. Furthermore, we describe specification formalisms for describing properties of OSGi based systems. One application is its use for behavioral types. Potential uses comprise the derivation of runtime monitors, checking compatibility of component composition, discovering components using brokerage services and checking the compatibility of implementation artifacts towards a specification. Consistency of component software is a crucial condition required for correct program execution. The existing consistency controls of OSGi at build time or in runtime cannot prevent type mismatch failures caused by independent client and server bundle development. This paper describes our solution to this problem using automated versioning of components. Version identifiers are generated from results of subtype-based comparison of component representations, thus achieving a consistent and formally backed interpretation of the version numbering scheme. The implementation of the approach allows its integration into standard OSGi bundle development and build cycle. The natural business model of OSGi is dynamic loading and removal of bundles or services on an OSGi platform. If bundles can come from different stakeholders, how do we make sure that one’s services will only be invoked by the authorized bundles? A simple solution is to interweave functional and security logic within each bundle, but this decreases the benefits of using a common platform for service deployment and is a well-known source of errors. Our solution is to use the Security-by-Contract methodology (SxC) for loading time security verification to separate the security from the business logic while controlling access to applications. The basic idea is that each bundle has a contract embedded into its manifest, that contains details on functional requirements and permissions for access by other bundles on the platform. During bundle installation the contract is matched with the platform security policy (aggregating the contracts of the installed bundles). We illustrate the SxC methodology on a concrete case study for home gateways and discuss how it can help to overcome the OSGi security management shortcomings. Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fix-point form. Then by successive (semi-dual) Galois connection based abstractions, type systems and or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new � la Church Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner Mycroft and Damas Milner polymorphic type schemes, Church Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.