Towards Formal Certification of Software Components
Software certification as it is practised today guarantees that certain standards are kept in the process of software development. However, this does not make any statements about the actual quality of implemented code. The authors propose an approach to certify the non-functional properties of component-based software which is based on a formal refinement calculus, using the performance abstractions of the Palladio Component Model. The certification process guarantees the conformance of a component implementation to its specification regarding performance properties, without having to expose the source code of the product to a certification authority.