Model Driven Development (MDD) has been slowly superseding traditional ways of developing embedded software in the recent decade. In line with the MDD, debugging Real-Time Embedded Software Systems (RTESS) and visualizing their behavior using models such as UML diagrams is becoming a reality. However, the existing MDD based debugging tools for RTESS are not applicable (require significant source code instrumentation, sophisticated debug interfaces, etc) for memory-size constrained RTESS. To address this, we discuss a model-based debugging methodology for RTESS which aims at overcoming the aforementioned limitations. Using our approach, the target behavior can be visualized in real-time using UML sequence and timing diagrams. We illustrate our approach with a prototype and examples. Performance metrics such as the target monitor size and the instrumentation overhead are discussed.

The behavior of commercial systems is described with business process models. There are different notations and formalism to express business processes. Many of these notations such as BPMN or ARIS EPC models are widely used in commercial projects. In the paper we focus on formalisms to express rules and specifications for the business processes. Temporal logic in general is a suitable formalism to express rules for dynamic processes. CTL is one kind of temporal logic focusing on branches and paths in particular. With CTL it is possible to formulate rules about different paths in business processes. Since the textual formulae of CTL are not very suitable in the development of commercial systems we introduce a graphical notation (G-CTL) based on the business process notation ARIS EPC. Moreover, we add to the CTL semantics specializers to differentiate between the element types in business process models and provide wildcards which allow the user to check for unknown elements or elements with only partially known properties.

System quality is a key issue in modern systems development. Tool support is essential for checking the system quality efficiently. This is particularly true with respect to the dynamic interactions of the processes within a system. A first generation of checkers - model checkers - provide a basic technology for the verification of process-based systems. Conventional model checkers bear two drawbacks concerning mainly their user-friendliness which impede their broad application. First, model checkers in general do not support the graphical representation of rules (specifications). Although a model may be described with a graphical notation the specification which has to be checked against the model is generally still text-based. This makes the usage of the checker difficult for process modeling experts. Second, the expressiveness concerning the verification model semantics to be checked is limited to states which are connected by transitions. However, many system development models (e.g. the business process model we use as example) embrace more element types. These are unsupported by the conventional model checkers resulting in a loss of verification precision. The checking system we present in this paper integrates both novelties: the graphical notation for a user-friendly specification and an extended specification language together with a corresponding verifier which supports the checking of many different types of elements (although the paper presents the approach with only two types). The integration is realized by an XML-based transformation system which links the graphical editor to the checking tool.

Business Process Management is a paradigm for enterprise computing that uses IT not only to support or execute business processes but also to continuously monitor and improve these processes to better achieve business objectives. A variant on Business Process Management, called Semantic Business Process Management, is meant to further close the gap between business and IT by attaching business semantics to the technology artifacts used for Business Process Management. A current problem in Semantic Business Process Management is that the specification of the business requirements that processes must respond to and that follow from the enterprise's strategic decisions, is not fully integrated within the design of the processes themselves. In this paper, we propose an approach in which business requirements for business processes are formally modeled and the skeleton of the designs of these business processes is automatically generated from these models. The approach presented here focuses upon the modeling of policies (i.e., a kind of business requirements for business processes) and on the subsequent design of business processes that comply to these policies. A first contribution is extending an existing goal-oriented requirements specification language, i.e. Formal Tropos, to incorporate policies, called Policy-extended Formal Tropos. A second contribution is offering an automated transformation to create business process design skeletons out of the Policy-extended Formal Tropos models. The paper also reports upon three pilot studies that were conducted as a first, though preliminary, empirical test of our approach.

In the software development (e. g. with product lines or refactoring) transformations play an increasing role. To ease and automate these transformations, we propose a solution based on the operator hierarchy concept. It allows to define transformation operator hierarchies containing different levels of transformation operators. The operators capture reusable knowledge units. The concrete realization of such a higher-level transformation language construction is demonstrated by an application of the XML operator hierarchy concept to the transformation language XSLT. XSLT serves as an example which is employed to provide the elementary transformation operators. On top of these elementary operators the layered concept allows the definition of new higher-level operators, e. g. domain-independent and domain-specific ones. In an application example the construction of the higher-level language XML2DSV is presented. This is a stand-alone domain-specific transformation language, which can be used to create delimiter-separated values (DSV) files from XML documents, on the base of XSLT. We developed XTC (XML Transformation Coordinator) to automate the multi-level transformation process.

Model-driven architecture aims at describing a system using a platform-independent model in sufficient detail so that the full implementation of the system can be generated from this model and a platform model. This implies that the platform-independent model must describe the static structure as well as the dynamic behavior of the system. We propose a declarative language for describing the behavior of platform-independent models based on a hybrid notation that uses graphical elements as well as textual elements in the form of OCL code snippets. Compared to existing approaches based on action languages it is situated at a higher level of abstraction and, through a clean separation of modifier operations and query operations, simplifies the comprehension of the behavioral aspects of the platform-independent system.

Many approaches such as component technologies have been invented in order to support software reuse. Based on these technologies a large variety of techniques have been introduced to connect components. However, there is little experience concerning the validation of component systems. We know how to plug components together, but we do need ways to check whether that works. In this paper we introduce an approach to validating component compositions and showing how such a process can be supported by tools. We introduce a way to compare the interface specification of components automatically against the code. Furthermore, we demonstrate how compositions of components can be specified by logical formulas, allowing us to automatically validate these compositions.