MSVVEIS 2010 Abstracts

Full Papers Short Papers
Full Papers
Paper Nr: 5
Title:

The Analysis of Resource Constrained Workflows Using Petri Nets
Authors:

Oana Prisecaru
Abstract: workflow describes a complex process that takes place inside an organization. A workflow can be structured into several perspectives. In order to model both the process and the resouce perspective of workflows, a Petri net model based on nested Petri nets has been proposed: resource workflow nets (RWF-nets). Unlike other models, RWF-nets permit a clear distinction between the perspectives, modelling efficiently their interaction, and ensure the flexibility of the system. A case (or workflow instance) is the subject of the operations in the workflow. RWF-nets permit the handling of one case at a time. This paper extends the definition of RWF-nets in order to allow the handling of multiple cases at a time, defines a notion of behavioural correctness for RWF-nets, $k$-soundness, and proves the decideability of this property for a special class of RWF-nets.
Download
Paper Nr: 6
Title:

KAOS-B: A Goal-Oriented Process Model for EIS
Authors:

Malihe Tabatabaie, Fiona Polack and Richard Paige
Abstract: In today’s software engineering domain there is an increasing demand for IT solutions to develop more effective enterprise information systems (EIS). One of the possible solutions to develop a better EIS focuses on goals prior to requirements. We believe that one of the challenges of EIS is lack of understanding of enterprise’s goals. Therefore, approaches that focus on investigating and structuring enterprise goals in early stage of software development could help the developer team and other stakeholders specially decision makers have a clear and structured understanding of enterprise’s goals. This solution leads to development of software systems that could satisfy the explicit feasible goals of enterprise. The focus of this paper will be on exploring KAOS approach to tailored it down using empirical studies. The goal is to illustrate KAOS- process model as an approach for defining and structuring the goals of groups of EIS.
Download
Paper Nr: 8
Title:

Extending CTL to Specify Quantitative Temporal Requirements
Authors:

Ammar Mohammed
Abstract: Computation tree logic (CTL) is expressive to specify those qualitative properties which focus on the temporal order of events. It, however, lacks to specify quantitative temporal requirements, which put time constraints on the occurrence of events. Thus, this paper presents a novel variant of temporal logic, RCTL (Region Computation Tree Logic), that extends CTL by incorporating the notation of time explicitly. To accomplish this aim, the paper uses hybrid automata as a model of computation. The specification language of RCTL allows us to express many properties in a concise and intuitive manner. To bring model checking within the scope of RCTL, the paper focuses on the specification of those properties that can be verified using reachability analysis, which is implemented in a previous work.
Download
Paper Nr: 9
Title:

Compositional Verification of Business Processes by Model-Checking
Authors:

Luis Eduardo Mendoza, María A. Perez and Manuel Isidoro Capel-Tuñón
Abstract: The work presented in this article is aimed at a contribution to the Enterprise Information Systems (EIS) verification. We describe here a Formal Compositional Verification Approach (FCVA) -based on Model-Checking (MC) techniques- applied to the verification of Business Process (BP) models represented by Business Process Modelling Notation (BPMN) diagrams. FCVA is compositional and thus allows the verification of a complex BP model carried out from verification of its parts. FCVA and a proposal of temporal semantics for BPMN allows the expression of time-dependent constructs of BP Task Models (BPTM) supported by an EIS. The interpretation of the BPMN graphical modelling entities into a formal specification language (CSP+T) allows us to use state-of-the-art MC tools to verify the behavioural part of BP models. A real-life example in the field of the Customer Relationship Management (CRM) business is presented to demonstrate the FCVA application in a practical way.
Download
Paper Nr: 10
Title:

Framework for Performance Evaluation of Service Negotiations in Agent Systems
Authors:

Costin Badica
Abstract: We propose a framework and method for evaluation of performance of multi-issue, collaborative service negotiations in multi-agent systems. The framework uses the following evaluation criteria: computation complexity, communication complexity, and scalability. Our proposal is applied to analyze a version of Contract Net protocol that we use in an agent system for disaster management. In particular we discuss how agents compute the additional e ort they must deploy to meet conditions of negotiation issues. Two negotiation issues specific to disaster management problems are given as example: location and time.
Download
Paper Nr: 12
Title:

Definition of Domain Specific Operation Languages following MDD
Authors:

Pedro P. Alarcon, Jennifer Pérez, Agustin Yague and David Musat
Abstract: Monitoring, testing and operation processes are essential tasks to ensure the correct behaviour of complex software systems. These processes are executed by operators using validation and operation (V&O) environments, which allow the interaction with systems. Operators are usually experts in the domain. Therefore, operators need to interact with the system by using Domain-Specific Operation Languages (DSOLs). Thus, a new challenge emerges: V&O environments should be adaptive to the interaction domain. However, the definition of DSOLs and their integration in V&O environments are usually done by hand. In this paper, we take a first step forward to cope with this challenge. A MDD process to semi-automate the definition of DSOLs is proposed. We focus on the definition of DSO Models to automatically generate DSOLs with the required information to integrate them in V&O environments. We present a framework that supports this solution, called ESPORA, through a case study of biogas plants.
Short Papers
Paper Nr: 7
Title:

Towards Domain-specific Modeling for Java Enterprise Applications
Authors:

Moritz Balz and Michael Goedicke
Abstract: Enterprise Applications are usually developed in the context of certain frameworks and platforms, for example the Java Enterprise Edition. These environments determine specific software architectures for such applications with respect to modularization, distribution, and interface provision, so that the structure of the applications is often very similar. However, so far no domain-specific models for these architectures exist. In this position paper we propose a domain-specific model for such applications that considers design information available as meta data in the program code. This will enable graphical design, verification, monitoring, and design recovery for this class of enterprise applications.
Download