Interface specification methods for software components

Abstract

This report presents an interface specification language developed as a part of the LIME-project (LightweIght formal Methods for distributed component-based Embedded systems) and a tool implementation to support it. The intention is to provide a methodology that is lightweight and complementary to the existing means of quality assurance in a software process.

The specification language provides a mechanism for specifying both external usage of a software component, as well as the internal behavior of a one. The former is referred to as interface specification, and the latter to as library specification. Should the interface specification be breached between two interacting components, the calling component is incorrect. Likewise, if the called component does not obey library specification, it will be the one to take the blame. Both types of specification can be written using either propositional linear temporal logic (PLTL) or by regular expressions, and may contain claims about the component's state or the currently executing method.

Java has been used as the implementation language on the approach because of the preexisting metadata mechanism (Java annotations) and good tool support. The tool implementation relies on aspect-oriented programming developed by Gregor Kiczales and his team at Xerox PARC in the late 90s. It employs annotation-guided generation of temporal safety aspects to synthesize the defined properties as behavioral invariants to the runtime execution of the program. The aspects simulate finite state automata which keep track of the state of the interaction and signal an exception in case of an error in it is observed.