Selected Publications

2005

•  G. Pintér and I. Majzik. Automatic Generation of Executable Assertions for Runtime Checking Temporal Requirements. In M. Dal Cin, A. Bondavalli, and N. Suri, editors, Proc. The 9th IEEE International Symposium on High Assurance Systems Engineering (HASE 2005), pages 111-120, Heidelberg, Germany, October 2005.
  BibTeX

  Abstract: Checking various temporal requirements is a key dependability concern in safety-critical systems. As model-checking approaches do not scale well to systems of high complexity the runtime verification of temporal requirements has received a growing attention recently. This paper presents a code-generation based method for runtime evaluation of linear temporal logic formulae over program execution traces. The processing-power requirements of our solution are much lower than in case of previous approaches enabling its application even in resource-restricted embedded environments.

•  G. Varró, A. Schürr, and D. Varró. Benchmarking for graph transformation. In Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC 05), pages 79-88, Dallas, Texas, USA, September 2005. IEEE Press.
  BibTeX

•  A. Balogh, D. Varró, and A. Pataricza. Model-driven optimization of enterprise application and service deployment. In Service Availability - Processdings of the 2nd International Service Availability Symposium (ISAS 2005), pages 84-98, April 2005.
  BibTeX

•  H. Ehrig, K. Ehrig, J. de Lara, G. Taentzer, D. Varró, and Sz. Varró-Gyapay. Termination criteria for model transformation. In Maura Cerioli, editor, Proc. FASE 2005: Internation Conference on Fundamental Approaches to Software Engineering, volume 3442 of LNCS, pages 49-63, Edinburgh, UK,, April 2005. Springer.
  BibTeX | .pdf

  Abstract: Model transformation has become central to most software engineering activities. It refers to the process of modifying a (usually graphical) model for the purpose of analysis (by its transformation to some other domain), optimization, evolution, migration or even code generation. In this work, we show termination criteria for model transformation based on graph transformation. This framework offers visual and formal techniques based on rules, in such a way that model transformations can be subject to analysis. Previous results on graph transformation are extended by proving the termination of a transformation if the rules applied meet certain criteria. We show the suitability of the approach by an example in which we translate a simplified version of Statecharts into Petri nets for functional correctness analysis.

•  G. Pintér, H. Madeira, M. Vieira, A. Pataricza, and I. Majzik. A Data Mining Approach to Identify Key Factors in Dependability Experiments. In M. Dal Cin, M. Kaâniche, and A. Pataricza, editors, Proc. Fifth European Dependable Computing Conference (EDCC-5), pages 263-280, Budapest, Hungary, April 2005.
  BibTeX

  Abstract: Our paper presents a novel approach for identifying the key infrastructural factors determining the behavior of systems in the presence of faults by the application of intelligent data processing methods on data sets obtained from dependability benchmarking experiments. Our approach does not rely on a-priory assumptions or human intuition about the dominant aspects enabling this way the investigation of highly complex COTS-based systems. The proposed approach is demonstrated using a commercial data mining tool from IBM on the data obtained from experiments conducted using the DBench-OLTP dependability benchmark. Results obtained with the proposed technique identified important key factors impacting performance and dependability that could not have been revealed by the dependability benchmark measures.

•  Z. Micskei. Automatic test generation using modell checkers. In Bitay E., editor, Proc. of X. Fiatal Mûszakiak Tudományos Ülésszaka (FMTU), pages 47-50, Kolozsvar, Romania, March 18-19 2005. Erdélyi Múzeum Egyesület.
  BibTeX

  Abstract: Testing is an essential, but time and resource consuming activity in the software development process. Generating a short, but effective test suite usually needs a lot of manual work and expert knowledge. In a model-based process, among other subtasks, test construction and test execution can also be partially automated. Based on the method suggested in [1], this paper presents a test generator tool, which can be used for test set generation in the development process of event-driven embedded systems. For a selected test coverage criterion and from the UML statechart model of the system the program generates test cases using the SPIN model checker. The test generator tool supports currently the test sequence construction on the basis of the “all states” and “all transitions” coverage criteria. The necessary model transformation [2] and requirement generation steps are performed automatically. The configuration of the model checker in the case of test generation, namely the settings required for constructing a short and minimal test suite, differs from the usual needs of classic model checking problems. The paper analyzes the possible settings of the model checker SPIN by measuring the efficiency of test construction in the case of different real-life statechart models, and introduces an optimized setting for test generation. The test generator is extended for real-time applications, in this case the model is available in the form of timed automata, and the model checker to be used is Uppaal [3].

•  A. Balogh. Viatra 2: Egy általános modell-transzformáció fejleszto keretrendszer (in hungarian). In Fiatal Mûszakiak Tudományos Ülésszaka Konferencia kiadványa. Erdélyi Múzeum Egyesület, March 2005.
  BibTeX

•  G. Pintér. Runtime Verification based on Abstract Models. In Fiatal Müszakiak Tudományos Ulésszaka X, pages 137-140, Cluj-Napoca, Rumania, March 2005. (In Hungarian).
  BibTeX

  Abstract: This paper outlines some achievements of our recent research related to run-time verification of UML statechart implementations. We present a verification framework offering a considerable degree of granularity by (i) enabling the specification of key dependability requirements in the early modeling phases by proposing a temporal logic language fitted to statecharts and (ii) by supporting the verification of the final implementation against the fully elaborated statechart model.

•  A. Balogh, A. Németh, A. Schmidt, I. Ráth, D. Vágó, D. Varró, and A. Pataricza. The VIATRA2 model transformation framework. In ECMDA 2005 - Tools Track, 2005.
  BibTeX

•  L. Gönczy. Dependability analysis of web service-based business processes by model transformations. In Proc. of the First European Young Researchers Workshop on Service Oriented Computing (YR-SOC), pages 32-37, Leicester, UK, 2005.
  BibTeX

  Abstract: A typical composite Web service is built of basic Web services, both internal and external, over which the integrator does not have a complete control. The service-based integration of enterprise systems raises the need for the analysis of non-functional characteristics of a composite Web service. Such an analysis should cover dependability (for instance, the reliability of the main process, sensitivity analysis on component reliability, etc.) and performability aspects (e.g. determining the optimal process structure for a given level of reliability) as well. The paper discusses how graph transformations can be used to adapt formal methodologies for analyzing SOA models. This way a flexible and extendable analysis framework can be developed for Web service-based business processes.

•  L. Gönczy, A. Pataricza, F. Di Giandomenico, S. Chiaradonna, and A. Bondavalli. Dependability modeling of web service flows. In In Supplementary Volume of the Fifth European Conference on Dependable Computing (EDCC-5), pages 77-78, Budapest, HUNGARY, 2005. Fast Abstract.
  BibTeX

•  K. Ehrig, E. Guerra, J. de Lara, L. Lengyel, T. Levendovszky, U. Prange, G. Taentzer, D. Varró, and Sz. Varró-Gyapay. Model transformation by graph transformation: A comparative study. In MTiP 2005, International Workshop on Model Transformations in Practice (Satellite Event of MoDELS 2005), 2005.
  BibTeX | .pdf

  Abstract: Graph transformation has been widely used for expressing model transformations. Especially transformations of visual models can be naturally formulated by graph transformations, since graphs are well suited to describe the underlying structures of models. Based on a common sample model transformation, four different model transformation approaches are presented which all perform graph transformations. At first, a basic solution is presented and crucial points of model transformations are indicated. Subsequent solutions focus mainly on the indicated problems. Finally, a first comparison of the chosen approaches to model transformation is presented where the main ingredients of each approach are summarized.

•  Zs. Pap, I. Majzik, A. Pataricza, and A. Szegi. Methods of checking general safety criteria in UML statechart specifications. Journal of Reliability Engineering and System Safety, 87(1):89-107, January 2005.
  BibTeX

•  I. Majzik and P. Domokos. Dependability modeling using aspect weaving techniques. In M. Dal Cin and A. Pataricza, editors, Proc. Fifth European Dependable Computing Conference, volume Supplementary Volume, pages 77-78, 2005.
  BibTeX

•  G. Pintér and I. Majzik. Modeling and Analysis of Exception Handling techniques by Using UML Statecharts. In Nicolas Guelfi, Gianna Reggio, and Alexander Romanovsky, editors, Scientific Engineering of Distributed Java Applications, pages 58-67. Springer-Verlag, 2005.
  BibTeX

  Abstract: Our paper aims at proposing a framework that allows programmers to exploit the benefits of exception handling throughout the entire development chain of Java programs by modeling exception handling in the abstract UML statechart model of the application, enabling the use of automatic model checkers for checking the behavioral model for correctness even in exceptional situations, and utilizing automatic code generators for implementing the Java source of exception-aware statecharts.

•  G. Pintér and I. Majzik. Run-time Verification of Statechart Implementations. In Cristina Gacek, Alexander Romanovsky, and Rogerio de Lemos, editors, Architecting Dependable Systems, pages 148-172. Springer-Verlag, 2005.
  BibTeX

  Abstract: Our paper introduces a run-time verification framework for concurrent monitoring of applications specified by UML statecharts. The approach offers a conside rable degree of granularity by (i) enabling the modeler to focus on specific key dependability criteria by defining temporal logic formulae over a behavioral model that is available even in early phases of the development and (ii) by supporting the verification of the final implementation against the fully elaborated UML statechart model. The paper presents an extension of the pro positional linear temporal logic that fits to the advanced constructs of UML statechart s and an advanced watchdog scheme for concurrent supervision of program execution bas ed on the statechart specification.

•  L. Baresi, R. Heckel, S. Thöne, and D. Varró. Style-based modeling and refinement of service-oriented architectures. Journal of Software and Systems Modelling, 2005. In press.
  BibTeX

•  L. Grunske, L. Geiger, A. Zündorf, N. Van Eetvelde, P. Van Gorp, and D. Varró. Model Driven Software Engineering, chapter Using Graph Transformation for Practical Model Driven Software Engineering, pages 91-118. Springer, 2005.
  BibTeX

•  A. Pataricza and D. Varró. Formal Methods in Computing, chapter Metamodeling and Model Transformations, pages 357-425. Akadémiai Kiadó, 2005.
  BibTeX

•  Sz. Varró-Gyapay and D. Varró. Simultaneous optimization and reachability analysis of schedulability problems in graph transformation systems with time. Journal of Software and Systems Modelling, 2005. Submitted paper.
  BibTeX

•  A. Balogh, G. Varró, D. Varró, and A. Pataricza. Model-based optimization of enterprise application and service deployment. In Miroslaw Malek, Edgar Nett, and Neeraj Suri, editors, Second International Service Availability Symposium, ISAS 2005, Berlin, Germany, April 25-26, volume 3694 of LNCS, pages 84-98. Springer, 2005.
  BibTeX

•  G. Varró, D. Varró, and K. Friedl. Adaptive graph pattern matching for model transformations using model-sensitive search plans. In G. Karsai and G. Taentzer, editors, GraMot 2005, International Workshop on Graph and Model Transformations, ENTCS, 2005. In press.
  BibTeX

•  T. Mens, P. van Gorp, G. Karsai, and D. Varró. Applying a model transformation taxonomy to graph transformation technology. In G. Karsai and G. Taentzer, editors, GraMot 2005, International Workshop on Graph and Model Transformations, ENTCS, 2005. In press.
  BibTeX

 

---