Related topics:

Model-Based Design of System Management
VIATRA: VIsual Automated model TRAnsformations
Model-driven development and analysis of Service Oriented Architectures
Integration of UML and formal analysis methods for assuring dependability
Recent projects using a combination of UML and formal methods

 

Model-Based Design of System Management

Traditionally, the configuration design of IT service and infrastructure management environments has been a process largely governed by heuristics. In the last few years it became evident that with the business of organizations relying more and more on their IT infrastructure there is a need for the verification and validation of the nonfunctional properties. These service level and information security requirements have to be satisfied in large, heterogeneous IT systems. However, with heuristic design of IT management configurations cannot cope with complex systems. We advocate to employ the Model Driven Design approach well-established by now in other fields to model, analyze and plan IT infrastructure management configurations.

In the engineering modeling domain, our research efforts involve hierarchical, multi-aspect system modeling. Known modeling languages as UML have to be extended by platform and application-platform interaction models in order to describe the nonfunctional characteristics of IT systems. Notably, our approach aims also at the integration of the software/service level with hardware models. A key goal is to model and analyze fine granular temporal and hardware redundancy.

In system-level analysis we did elaborate qualitative techniques, where complex errors/incidents/performance characteristics are automatically abstracted into a small set of qualitative values. Completeness and consistency of the reactions of supervisory systems can be ensured by existing formal analysis methods, like model checking. This research area is strongly connected to the FP6 IP EU project DESEREC - Dependability and Security through Advanced Reconfigurability. Also, this is a key area where we collaborate with the IBM Center of Advanced Studies Budapest.

 

 

VIATRA: VIsual Automated model TRAnsformations

One of the main conclusions of the HIDE project was that the implementation of complex transformations necessitates a mathematically precise formulation of the transformation rules and the transformations have to be generated automatically from these rules. VIATRA is a general purpose model transformation engine that is designed to automate transformations specified by graph transformation rules between models defined by their corresponding metamodels.

Its primary target application field is to provide a transformation based verification and validation of system models designed in UML, where UML models are projected automatically into various mathematical domains (such as Petri nets, dataflow networks, hierarchical automata), and the results of the formal analysis are back-annotated to the UML level, thus the underlying mathematical background is completely hidden to the system engineer.

According to the main design goals of the framework, VIATRA should provide

Publications

In the following, an annotated list of main publications on VIATRA is given. In each section, papers are arranged in a recommended order for reading.

Introduction and overall concepts

The following papers provide an introductory overview of the VIATRA framework from an engineering point of view (thus with few mathematical details).

Semantic foundations

The formal semantics of VIATRA based upon model transition systems (which is the combination of metamodeling and graph transformation with explicit control structures) is defined by the following papers.

Automated program generation

From a high-level visual representation of transformation rules and control structures (in the form of a special UML profile tailored to model transition systems), the transformation engine can be generated automatically in the form of a Prolog program that will project arbitrary source models into their target equivalent.

Proving correctness of transformations

For obtaining a proven quality of transformations, not only models but their transformations are required to be verified. When proving syntactic correctness and completeness, we have to decide e.g., whether the output of the transformation is a well-formed model of the target language. However, for semantics correctness we have to show that certain properties are preserved by the transformation.

Metamodeling and model semantics in VIATRA

VIATRA is not only a framework for describing transformations between different modeling languages, but we can also define operational semantics of these languagesby graph transformation rules driven by a control structure.

Standardization of graph transformation systems

We participate in the standardization committee organized by the Appligraph network of excellence that aims at the creation of GXL-GTXL, an XML based interchange format for graphs, and graph transformation systems. The following two technical reports form the Budapest proposal that was presented during the Paderborn and the Bremen meeting.

 

 

Model-driven development and analysis of Service Oriented Architectures

Nowadays, the paradigm of Service Oriented architecture is one of the main drivers of system development and integration. However, the present modeling and development techniques do not support the precise analysis of functional correctness and non-functional requirements (e.g. availability, performance, security, SLA parameters, etc.). Therefore, there is an urgent need to integrate the current modeling methodologies with precise formalisms.

The SENSORIA integrated project aims at developing a modeling approach and description language for service oriented systems. Our role is the description and verification of the dynamic behavior of fault-tolerant services, investigating model transformations for the analysis and deployment of services. We also participate in the development of a demonstrator to illustrate the integrated service engineering process.

 

 

Integration of UML and formal analysis methods for assuring dependability

The main trend in modern system design is the model driven development of the designated target application. This strategy uses a gradually refined set of semi-formal specifications starting from the initial requirements to define the IT implementation. UML, the Unified Modeling Language, offers a standard graphical notation covering the entire design life cycle. During the last five years, it became obvious that the main advantage of using a semi-formal modeling paradigm is the possibility to analyze the model from the point of view of correctness and conformance to the requirements. Recent standardization efforts at OMG aim at such extensions of UML that can serve as a basis for the mechanized proof of correctness of UML models.

However, the modeling of dependability attributes is still in its infancy (OMG just issued a request for proposals for modeling fault tolerance in UML). The Fault-Tolerant Systems Research Group at the Department of Measurement and Information Systems deals together with several national and international research partners with the problem of integrating the UML based modeling technology with formal analysis methods.

The approach used in our projects is to enrich the UML model with the local quality of services parameters relevant to a specific analysis objective (for instance, failure/repair rates are associates with the element in the UML model) and to automatically transform the relevant parts of the enriched UML model to a COTS analysis program. The results will be back annotated to the original model.

The basic idea

This research was carried out initially in co-operation with the Department of Computer Structures, University of Erlangen, Germany; Pisa Dependable Computing Centre, Italy; Intecs Sistemi SpA, Italy and MID GmbH, Germany in the framework of the project ESPRIT Open LTR 27439 "High-level integrated design environment for dependability (HIDE)".

Additionally to the feasibility study of the approach, some pilot transformations were defined and implemented.

Publications

The concepts of HIDE was presented in the following papers: The definition of a formal semantics of UML statecharts and the first transformation towards a models checker are documented in: Based upon the semantics introduced above, a proposal was elaborated at the BUTE for the self-checking implementation of a statechart runtime system: Performance analysis was introduced originally in HIDE and continued in a bilateral co-operation with the Friedrich-Alexander University of Erlangen-Nürnberg: Quantitative dependability assessment by mapping UML designs into stochastic Petri-Nets (modeling fault and repair processes) was introduced in:

 

 

Recent projects using a combination of UML and formal methods

Framework for the development and testing of dependable and safety critical systems

The main objective of this project which is carried out in co-operation with PROLAN Process Control Co., B-Braun Medical Hungary Ltd. and Magic ONYX Hungary Ltd. is to create a comprehensive framework to check the correctness of UML based designs and to validate the approach on industrial pilot examples (artificial kidney controller, railway interlocking system). Our approach aims at the extension of UML-based design environments by model based mathematical analysis and validation. The automatic model transformations, the applied formal analysis tools and the back-annotation of the results ensure the checking of the completeness and consistency of the specification (by applying Nancy Leveson's principles to UML statecharts) as well as the easy verification of behavioral properties (by he application of efficient semi-decision methods in the verification process), and dependability-related characteristics  of the design (by activity diagram based fault modeling and analysis of error propagation and testability).

Publications

BPM based development of robust e-business applications

The objective of the research project under our internal acronym "e-Balaton" is to create such an environment, which can analyze the correctness of business process models described in UML even in the presence of faults, to optimize their resource utilization and to couple this UML-based design flow with an industrial e-Business tool. The project partners are the Department of Computer Science, the Department of Tourism, both at the University of Veszprém, and Balatourist Co, the largest accommodation provider at the northern coast of the Lake Balaton.

Publications

Integrated project management optimization

The objective of the joint project with  University of Veszprém, Department of Computer Science, AAM Management Information Consulting Ltd., and  Sysdata Information Technology Ltd. (a subsidiary of Siemens) is a unified framework, where cost estimators are assigned to the individual components in the UML based design. From  this the total implementation cost is forecasted for the entire design by using standard cost estimation models, like COCOMO, COCOTS etc. This model is  refined by allowing a hierarchical decomposition of the design process , similarly described in UML. A personal database supplies human resource related information. A combined model merging these three information sources serves as a starting point for the estimation of the development time, its optimal scheduling and development cost minimization.
 

Publications

UML Based Modelling and Design of Technological Processes

Two national projects accompanied by a Hungarian-German researchers exchange program with the Friedrich-Alexander University Erlangen-Nuremberg, Inst. of Computer Science aims at a harmonization of the design process of embedded industrial control systems and the modern software engineering methods, as well as optimizing them and promoting the reliability of these systems by automatic analysis of the effects of potentially arising faults. Our goal is the extension of the current  knowledge in the field of fault modeling, together with contribution to the qualitative and quantitative reliability analysis.

Publications

 

Dániel Varró and András Pataricza

 

Valid HTML and CSS