by Tomáš Bureš and Petr Hnětynka
Embedded devices like mobile phones, PDAs, set-top boxes and vehicular systems are now an inherent part of daily human life. However, software for these devices must meet additional requirements compared to desktop and server computers. We present the SOFA 2 component system, which is suitable for building safe and configurable applications.
As embedded devices become ubiquitous, the efficient and error-free development of the necessary software is becoming increasingly important. While a given device will operate in a very similar environment to others of its kind (eg mobile phones, consumer electronics or vehicular systems), it may differ in specific details. Typically, there exists a common core for a family of devices, and a set of optional extensions whose presence depends on the available hardware (eg the presence of Bluetooth in mobile phones, air-conditioning in cars etc) or other requirements. One approach to this situation is 'software product lines', which allows the specification of not just one system, but the whole family of systems. However it places strong requirements on the software development platform for support for the configuration of application variants.
Also commonly required of embedded software is support for functional and safety verification (a necessity for software in, for example, vehicles). This requirement is reflected in the need for a formal specification of system behaviour, verifications of the specification and so forth.
A relatively recent approach to coping with complexity, variability and safety in embedded systems is the use of component-based development (CBD), which employs well-defined components as reusable basic building blocks. It also carefully captures the dependencies and interactions between components, which helps to mitigate the complexity.
SOFA 2 (SOFtware Appliances version 2) is one representative of existing advanced approaches to component use. It was designed and developed by the Distributed Systems Research Group at Charles University in Prague. It features a modern component model and a software development platform. Among other capabilities, it provides hierarchical component composition, software connectors, dynamic architectures and formal specifications of behaviour.
SOFA 2 fully satisfies both of the above-mentioned requirements (modelling of variability and the use of formal methods to ensure safety). The former is satisfied by distinguishing three separate steps in system development: definition of components, their assembly into a final system, and system deployment. The latter requirement is satisfied by inherent usage of formal specifications and verification of component behaviour.
Development of a system in SOFA 2 is quite straightforward and is performed chiefly by composing existing components available in the SOFA 2 repository. The development process starts with the definition of the architecture of a system. Using development tools, a developer can browse the repository content and compose existing components, or build new ones. The individual components are defined by a 'component type' and 'component implementation' (which implements a particular component type). The implementation is either direct (in a programming language) or composed from other components. These 'sub-components' are themselves defined by component types.
This separation is crucial for the support of product line development. Developers can develop a set of basic (direct) components that provide building blocks of systems. For each component type, there can be several different implementations that meet specific requirements. In the assembly part of the development process, the component types in a composite component are 'refined' by chosen component implementations. This assembly process starts with the top-level component (that represents a complete system) and recursively continues down to the basic components. When the system is fully assembled, it can be deployed in a target environment. SOFA 2 inherently supports distributed systems, and the distribution is completely transparent to developers. This is achieved thanks to automatically generated software connectors that, based on final deployment, provide either local or remote calls between components.
For verification of component behaviour, SOFA 2 employs 'software behaviour protocols'. These are simple process algebra, which defines the externally observable behaviour of a component type, and are used to verify several properties. First, for the composite components, they are used to determine whether the sub-components of a composite component are composed correctly and together implement the required behaviour. For the basic components, one can verify that the required protocol is correctly implemented. In addition, the protocols can be used during development for testing whether the actual observed behaviour of a component complies with the protocol.
The decomposition of a system to its components makes it possible to perform verification of relatively large systems. This would be unfeasible if the system were viewed as a monolithic block, due principally to the exponential complexity of the verification algorithms.
SOFA 2 is implemented in Java and is freely available (together with the source code) from its Web page, which is part of the OW2 international consortium (formerly ObjectWeb). The downloadable packages contain the runtime environment for executing components, a repository for storing components, and development tools for creating components and verifying behaviour. Also available are ready-to-run examples, documentation and publications describing in detail the principles of SOFA 2 and its implementation.
Links:
SOFA 2: http://sofa.ow2.org
Distributed Systems Research Group: http://dsrg.mff.cuni.cz
Please contact:
Tomáš Bureš
Charles University Prague/CRCIM, Czech Republic
Tel: +420 221914236
E-mail: bures
dsrg.mff.cuni.cz
