Selected Publications

2003

• L. Baresi, R. Heckel, S. Thöne, D. Varró:
  Modeling and Analysis of Architectural Styles Based on Graph Transformation.
  Appeared in the 6th ICSE Workshop on Component Based Software Engineering: Automated Reasoning and Prediction, Portland, Oregon, USA, May 3-4, 2003
  BibTex

  Modern architectural styles, like the service-oriented style underlying web services, are highly dynamic. This complicates not only their practical application, but also the modeling and prediction of their behavior. To account for this problem, we propose to model architectures as graphs, represented as instances of UML class diagrams, and to describe their reconfigurations by graph transformation rules. Based on a sample model for service-oriented architectures, we discuss what are interesting properties to be analyzed and how such analysis could be performed.

• L. Baresi, R. Heckel, S. Thöne, D. Varró:
  Modeling and Validation of Service-Oriented Architectures: Application vs. Style.
  Accepted for ESEC 2003 Fourth European Software Engineering Conference, Helsinki, Finland, September 1-5, 2003
  BibTex

  Most applications developed today rely on a given middleware platform which governs the interaction between components, the access to resources, etc. To decide, which platform is suitable for a given application (or more generally, to understand the interaction between application and platform), we propose UML models of both the architectural style of the platform and the application scenario. Based on a formal interpretation of these as graphs and graph transformation systems, we are able to validate the consistency between platform and application. The approach is exemplified by means of an application scenario from a supply chain management case study using the service-oriented architectural style. In particular, we demonstrate the potential of model checking for graph transformation systems for answering the above consistency question.

• Sz. Gyapay, R. Heckel, D. Varró:
  Graph Transformation with Time.
  Invited to the International Journal of Fundamenta Informaticae
  BibTex

  Following TER nets, an approach to the modelling of time in high-level Petri nets, we propose a model of time within (attributed) graph transformation systems where logical clocks are represented as distinguished node attributes. Corresponding axioms for the time model in TER nets are generalised to graph transformation systems and semantic variations are discussed. They are summarised by a general theorem ensuring the consistency of temporal order and casual dependencies. The resulting notions of typed graph transformation with time specialise the algebraic double-pushout (DPO) approach to typed graph transformation. In particular, the concurrency theory of the DPO approach can be used in the transfer of the basic theory of TER nets.

• Sz. Gyapay, A. Pataricza:
  Optimization methods for reachability analysis of Petri net models.
  in G. Tarnai and E. Schnieder (eds.): Formal Methods for Railway Operation and Control Systems (Proceedings of Symposium FORMS-2003, Budapest, Hungary, May 15-16), pp.53-60, 2003, L' Harmattan, Budapest.
  

  Model based synthesis of IT systems especially of embedded systems is a more and more crucial task in order to assure the productivity of the design flow and the quality of the product. A proper proccessing of incoming requests has to be assured by the system specification. Recently, optimization is an additional focal task in guaranteeing an efficient operation of the system. Petri nets are widely used as a formal specification methodology. By extending Petri nets by cost and time parameters, they are appropriate to solve resource allocation and scheduling problems, as well. One of the main advantages of the use of Petri nets as modeling paradigm is the support by a wide variety of Petri nets analysis methods, especially useful in the verification of the system architecture. The current paper proposes efficient optimization and verification techniques by adopting the process network synthesis paradigm for reachability problems in Petri nets.

• Sz. Gyapay, A. Pataricza:
  A Combination of Petri Nets and Process Network Synthesis
  In Proc. of IEEE International Conference on Systems, Man & Cybernetics, Invited Sessions/Track on "Petri Nets and Discrete Event Systems", pp. 1167-1174, Washington, D.C., USA, October 5-8., 2003
  BibTex

  Resource allocation and scheduling optimization problems are core problems in the field of IT systems. However, such problems frequently underlie several additional constraints. The formalization of a real life problem requires a well-defined mathematical and modeling approach providing an integrated verification and optimization. The current paper proposes such methods adapting Process Network Synthesis algorithms to Petri net reachability problem: combining the efficiency of PNS optimization algorithms with the modeling power of Petri nets. They provide powerful techniques to compute optimal trajectories for the reachability analysis of the modeled system.

• A. Pataricza, I. Majzik, G. Huszerl, Gy. Várnai:
  UML-based Design and Formal Analysis of a Safety-Critical Railway Control Software Module.
  in G. Tarnai and E. Schnieder (eds.): Formal Methods for Railway Operation and Control Systems (Proceedings of Symposium FORMS-2003, Budapest, Hungary, May 15-16), pp.125-132, 2003, L' Harmattan, Budapest.
  BibTex

  A new equipment of safety relevance has been developed to upgrade ageing relay-based railway interlocking systems in Hungary. In course of the design process formal methods have been used in the development of a module realising a well-separable function of the system. Namely, the UML-based design process was extended by model based analysis and validation. The first kind of analysis checked the completeness and consistency of the behavioural description of the module. In the subsequent phases, the functional design was enriched by modelling the potential faults and their effects. This kind of extension allowed the analysis of the error propagation and testability.

• G. Pintér, I. Majzik:
  Automatic Code Generation Based on Formally Analyzed UML Statecharts.
  in G. Tarnai and E. Schnieder (eds.): Formal Methods for Railway Operation and Control Systems (Proceedings of Symposium FORMS-2003, Budapest, Hungary, May 15-16), pp.45-52, 2003, L' Harmattan, Budapest.
  BibTex

  This paper aims at providing an efficient implementation pattern for source code level instantiation of UML statecharts. The code generation is based on extended hierarchical automata, the formal description method used as an intermediate representation of statecharts for model checking purposes, this way enabling automatic implementation of formally analyzed models. Since statecharts can automatically be mapped to extended hierarchical automata, a code generator based on our pattern could be used as a module that can be inserted into any UML modeling tool equipped with model export capabilities. This approach enables the modeler to use the usual design environment and hides the transformation required for model checking and code generation steps.

• G. Pintér, I. Majzik:
  Program Code Generation based on UML Statechart Models.
  Submitted to the International Journal of Periodica Polytechnica
  BibTex

  Since visual modeling languages are getting more and more popular, automatic generation of program code on the basis of high-level models is an important issue. This article discusses implementation possibilities of statecharts, the graphical notation for describing state-based event-driven behavior in the Unified Modeling Language (UML). The first part of the article outlines common approaches published in the literature and identifies their weaknesses. In the second part an implementation pattern is proposed that is capable of efficiently instantiating most of the statechart features. The pattern developed by us poses low hardware requirements therefore applicable even in embedded systems.

• G. Pintér, A. Pataricza:
  Data Mining in Fault Injection.
  The 6th IEEE International Workshop on Design and Diagnostics of Electronic Circuits and Systems, April 14-16, 2003, Poznan, Poland.
  BibTex

  This paper outlines a method and environment for reflecting the effects of faults in the behavioral software models providing a way for building abstract reusable fault models that are applicable even in early phases of the software development. The main focus is on the application of intelligent data processing methods for extracting important phenomena from the database of fault injection experiments.

• G. Pintér, A. Pataricza:
  A Methodology for Benchmarking-based Abstract Fault Modeling.
  Accepted fast abstract in the IEEE International Conference on Dependable Systems and Networks, June 22-25, 2003, San Francisco, CA, USA.
  BibTex

  This paper presents a method and environment for embedding the high-level manifestation of low-level (physical) faults into the behavioral software model in the form of in abstract reusable fault models. The main focus is on the application of intelligent data processing methods for extracting important phenomena from the observations in fault injection experiments.

• A. Schmidt, D. Varró:
  CheckVML: A Tool for Model Checking Visual Modeling Languages (Tool demonstration)
  Accepted to UML 2003 International Conference on the Unified Modeling Language, October 20-24, 2003, San Francisco, CA, USA.
  BibTex

  In the paper, we present a tool for model checking dynamic consistency properties in arbitrary well-formed instance models of any modeling language defined visually by metamodeling and graph transformation techniques. Our tool first translates such high-level specifications into a tool independent abstract representation of transition systems defined by a corresponding metamodel. From this intermediate representation the input language of the back-end model checker tool (i.e., SPIN in our case) is generated automatically.

• A. Tóth, D. Varró, A. Pataricza:
  Model-Level Automatic Test Generation for UML Statecharts.
  The 6th IEEE International Workshop on Design and Diagnostics of Electronic Circuits and Systems, April 14-16, 2003, Poznan, Poland.
  BibTex

  We present a framework for model-level testing of behavioral UML models. For automatic test generation, we use planner algorithms to deal with the complexity of UML models. Our approach is characterized by an automatic and metamodeldriven transformation from UML statecharts to a tool independent representation of planner algorithms from which the input language of concrete planner tools can be easily derived. As a result, UML based system models can be tested in an early phase of the design prior to implementation.

• D. Varró, A. Pataricza:
  VPM: Mathematics of Metamodeling is Metamodeling Mathematics
  Journal of Software and Systems Modelling, Special Issue on UML 2002, Springer. (in press)
  BibTex

  As UML 2.0 is evolving into a family of languages with individually specified semantics, there is an increasing need for automated and provenly correct model transformations that (i) assure the integration of local views (different diagrams) of the system into a consistent global view, and, (ii) provide a well–founded mapping from UML models to different semantic domains (Petri nets, Kripke automaton, process algebras, etc.) for formal analysis purposes as foreseen, for instance, in submissions for the OMG RFP for Schedulability, Performance and Time. However, such transformations into different semantic domains typically require the deep understanding of the underlying mathematics, which hinders the use of formal specification techniques in industrial applications. In the paper, we propose a multilevel metamodeling technique with precise static and dynamic semantics (based on a refinement calculus and graph transformation) where the structure and operational semantics of mathematical models can be defined in a UML notation without cumbersome mathematical formulae.

• D. Varró, A. Pataricza:
  UML Action Semantics for Model Transformations
  International Journal of Periodica Politechnica (in press).
  BibTex

  The Action Semantics for UML provides a standard and platform independent way to describe the behavior of methods and executable actions in object-oriented system design prior to implementation allowing the development of highly automated and optimized code generators for UML CASE tools. Model transformation systems provide visual but formal background to specify arbitrary transformations in the Model Driven Architecture (the leading trend in software engineering). In the current paper, we describe a general encoding of model transformation systems as executable Action Semantics expressions to provide a standard way for automatically generating the implementation of formal (and provenly correct) transformations by off-the-shelf MDA tools. In addition, we point out a weakness in the Action Semantics standard that must be improved to achieve a stand-alone and functionally complete action specification language.

• D. Varró, A. Pataricza:
  Automated Formal Verification of Model Transformations
  Submitted to CSDUML 2003 Workshop on Critical Systems Development with UML, October 20-24, 2003, San Francisco, CA, USA.
  BibTex

  When designing safety critical applications in UML, the system models are frequently projected into various mathematical domains (such as Petri nets, transition systems, process algebras, etc.) to carry out a formal analysis of the system under design by automatic model transformations. Automation surely increases the quality of such transformations as errors manually implanted into transformation programs during implementation are eliminated; however, conceptual flaws in transformation design still remain undetected. In this paper, we present a meta-level and highly automated technique to formally verify by model checking that a model transformation from an arbitrary well-formed model instance of the source modeling language into its target equivalent preserves (language specific) dynamic consistency properties. We demonstrate the feasibility of our approach on a complex mathematical model transformation from UML statecharts to Petri nets.

• D. Varró:
  Towards Automated Formal Verification of Visual Modeling Languages by Model Checking
  Accepted to the Journal of Software and Systems Modelling, Special Issue on Graph Transformation and Visual Modelling Techniques, Springer.
  BibTex

  Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (i) requirements or behavior of user models (on the model-level), and (ii) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). In the paper, we present a meta-level transformation technique to enable model checking-based symbolic verification for arbitrary well-formed models and modeling languages (with formal semantics defined by graph transformation systems) by projecting them into state transitions systems that serve as the underlying mathematical specification formalism of various model checker tools. The feasibility of our approach is demonstrated by modeling and analyzing a well-known verification benchmark both on the model and metamodel level.

 

---