Towards Automated Checking of Component-Oriented Enterprise Applications

Reference:

Jukka Järvenpää and Marko Mäkelä. Towards automated checking of component-oriented enterprise applications. In Daniel Moldt, editor, Second Workshop on Modelling of Objects, Components and Agents, volume PB-561 of DAIMI report, pages 67–85, Århus, Denmark, August 2002. University of Århus.

Abstract:

Building enterprise applications using component-based frameworks has been suggested as a way to help companies manage their software assets. We propose tool support for managing these high-level data-centric applications with formal methods. Our method is based on extracting a system model from the models of components and from the application code which glues the components together. This model is used for generating state spaces that can be checked for desired or undesired properties. In order to manage the state space explosion problem we propose that the application developer controls some parameters of the model. Even though the insight of the application developer is still needed, we believe that creating tool support for the proposed method could contribute to the success of the component-based approach.

Keywords:

software components, transactions, abstractions, verification, Java

Suggested BibTeX entry:

@inproceedings{MakelaMarko-Jarvenpaa-Makela,
    address = {{\AA{}}rhus, Denmark},
    author = {Jukka J{\"a}rvenp{\"a}{\"a} and Marko M{\"a}kel{\"a}},
    booktitle = {Second Workshop on Modelling of Objects, Components and Agents},
    editor = {Daniel Moldt},
    month = {August},
    pages = {67--85},
    publisher = {University of {\AA{}}rhus},
    series = {DAIMI report},
    title = {Towards Automated Checking of Component-Oriented Enterprise Applications},
    volume = {PB-561},
    year = {2002},
}