@inproceedings{
    Jarvenpaa-Makela,
    editor = "Moldt, Daniel",
    author = {J{\"a}rvenp{\"a}{\"a}, Jukka and M{\"a}kel{\"a}, Marko},
    publisher = "University of {\AA{}}rhus",
    title = "Towards Automated Checking of Component-Oriented Enterprise Applications",
    series = "DAIMI report",
    booktitle = "Second Workshop on Modelling of Objects, Components and Agents",
    address = "{\AA{}}rhus, Denmark",
    month = "August",
    volume = "PB-561",
    flags = "public",
    pages = "67--85",
    year = "2002",
    keywords = "software components, transactions, abstractions, verification, Java",
    pdf = "mola.pdf",
    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."
}