Checking Non-functionalPropertiesInTheKoalaDomain
Stc
Date: Jan 31
Time: 12:00
Room: BBL room 471
Speaker: Tom Höfte
Title: Checking non-functional properties in the Koala domain
Abstract
Within Philips a light-weight component model, called Koala, is used
to develop TV software. The Koala Component Model comes with the Koala
Description Language. This architectural description language (ADL)
defines how the components are related to each other and what
functionalities a component requires and provides via its requires and
provides interfaces. The Koala compiler generates from a Koala model a
bunch C-header files that define the interface bindings by using macro
definitions.
Within the static program analysis project Amber a tool set for
analyzing the execution architecture has been developed, which uses as
starting point the C-files to check several non-functional properties,
like thread-safeness.
In this thesis project, two analysis tools has been designed and
implemented to check the non-functional properties thread-safeness and
deadlock in the Koala domain.
Within the Koala-domain, non-functional properties of the
C-implementation of the components are not known. Type annotations are
used to express the
non-functional properties of a Koala component so that we are able to
reason about them. Each analysis uses a type system to check for
inconsistencies.
Additionally, for the deadlock analysis a tool is developed that, on
one hand, can generate the type annotations of a component from its
C-module files and, on the other hand, can use these generated
annotations to check if the implementation of a component adheres
to the specification of the component.
All the tools are developed in the functional programming language
Haskell in combination with the Attribute Grammar (AG) system of the
University of Utrecht.
