TCS / Research / Publications / Interface Specification Methods for Software Components
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Interface Specification Methods for Software Components


Jani Lampinen. Interface specification methods for software components. Research Report TKK-ICS-R4, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, June 2008.


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.


Lightweight methods, Interface specification, Java, PLTL, Aspect-oriented programming

Suggested BibTeX entry:

    address = {Espoo, Finland},
    author = {Jani Lampinen},
    institution = {Helsinki University of Technology, Department of Information and Computer Science},
    month = {June},
    number = {TKK-ICS-R4},
    pages = {vi+49},
    title = {Interface Specification Methods for Software Components},
    type = {Research Report},
    year = {2008},

NOTE: Reprint of Master's thesis
PostScript (961 kB)
GZipped PostScript (387 kB)
PDF (492 kB)

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.