Semantics of software components for robot manipulation

Complex systems need to be designed and implemented by plugging together software components in a domain-specific architecture. This approach can only succeed fully if the designer understands the behavior of the software components and the conditions in which they can be used and, more importantly, re-used. For robotic manipulation, these semantics are, for example, conventions of dimensions and units, geometrical reference frames or the mathematical properties of matrices and vectors. This dissertation proposes a way to describe these semantics formally, so that violations in the use of the components can be caught during the design and so that components can adjust their implementation to the way they are used. This is done in the context of a specific architecture, the monotonic signalflow architecture. In this architecture, the components are functional blocks that interact through signals. This architecture is very useful in the design of real-time systems that interact with the physical world, such as robots. The semantics of this architecture are carefully defined and a new formal language, the Requirement/Assertion Description Logic (RADL) is proposed, to capture the semantics of components in this architecture. The semantics of RADL itself are rigorously defined using a model-based approach. Using these semantics means that, while plugging together components, the designer builds a rich database of information about the design. Because of the large size of this semantic database, an automatic reasoning tool is needed that combines the semantics of the individual components (expressed in RADL) with the way the components are used and inter-connected. A prototype reasoning tool for RADL was developed. This tool tries to find a good balance between fast reasoning and complete reasoning and shows that these kinds of techniques can enable large-scale development with powerful reusable and self-configuring software components.