This paper presents a methodology to extend the OMG General Resource Modeling sub-profile to model component faults in a UML design. This extension introduces the notion of faults into the resources. The UML model of the target system is extended by the description of the error propagation attributes of the different objects. A qualitative abstraction supports a semi-decision style approximate analysis of the effects of local faults to the dependability attributes, like safety requirements of the systems.
The paper presents techniques to support the dependability modeling and analysis of distributed object-oriented applications that are designed according to the Fault Tolerant CORBA (FT-CORBA) specification. First the construction of a high-level dependability model is described. It is based on the architecture of the application and allows the analysis of the fault tolerance strategies and properties that are directly supported by the standard infrastructure. Then a technique to construct a refined dependability model is presented. It exploits the detailed behavioral model of the object responsible for replica maintenance. The UML statechart of this object is transformed to a stochastic Petri net that forms the core of the dependability model. In this way the designer is allowed to utilize the full power of statecharts to construct models of application-dependent replication strategies and recovery policies.
This paper presents a method for verification of UML statechart models generated in the development process of embedded systems containing hardware and software components. The method allows the automated verification of behavioral requirements through model transformation and application of an off-the-shelf model checker. The transformation tools have been implemented and the method was applied successfully in the design verification of an interrupt controller. The paper deals with the details of the verification method and introduces the application example as well.
The VIATRA (VIsual Automated model TRAnsformations) framework is the core of a transformation-based verification and validation environment for improving the quality of systems designed using the Unified Modeling Language by automatically checking consistency, completeness, and dependability requirements. In the current paper, we present an overview of (i) the major design goals and decisions, (ii) the underlying formal methodology based on metamodeling and graph transformation (iii) the software architecture based upon the XMI standard, (iv) and several benchmark applications of the VIATRA framework.
Petri nets are widely used as an underlying framework for formalizing UML-based system models. Based on their precise semantics and easy-to-understand graphical representation, they are appropriate to model production systems together with their quantitative properties. The production of desired materials can be formulated as a reachability problem of its Petri net model, which can be analyzed by linear algebraic techniques (solving linear inequality systems). However, traditional reachability analysis techniques can result in a state-space explosion, while numerical methods for invariant computations give either sufficient or necessary conditions. Process Network Synthesis (PNS) algorithms are widely used in chemical engineering to estimate optimal resource allocation and scheduling in order to produce desired products from given raw materials. Moreover, PNS algorithms that exploit the specific combinatorial features of PNS problems can be applied to Petri nets in order to give more efficient mathematical methods for their analysis.The current paper presents efficient semi-decision and optimization methods for the reachability problem based on PNS algorithms: Solution Structure Generation (SSG) and Accelerated Branch and Bound (ABB) algorithms. We show that the ABB algorithm can be used to solve scheduling problems efficiently and can be extended for other Petri net analysis. Obviously, the combined methodology can be used for a variety of application fields like IT systems, workflow optimization, etc., including production processes as a special case.
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 time stamps 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. 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.
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. 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.
The paper introduces a method which allows quantitative dependability analysis of systems modeled by using the Unified Modeling Language (UML) statechart diagrams. The analysis is performed by transforming the UML model to stochastic reward nets (SRNs). A large subset of statechart model elements is supported including event processing, state hierarchy and transition priorities. The transformation is presented by a set of SRN patterns. Performance-related measures can be directly derived using SRN tools, while dependability analysis requires explicit modeling of erroneous states and faulty behavior.
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 initial phase of development. The lecture will present an overview on the state-ofthe- art dependability modeling techniques.
Nowadays formal methods and analysis techniques in design and modelling of modern computer controlled systems become more and more important. To provide easy-to-use tools for ensuring the overview of complex systems, multi-aspect modelling languages are specified (e.g. the Unified Modeling Language - UML). While focusing on best capturing the complex functionality, these languages neglect non-functional aspects such as quality of service - performance and dependability. However, during the modelling and design process, the specification of functional requirements is often insufficient. To deal with performance and dependability of systems the modelling languages should have an integral part of the notation for describing the quantitative properties of model elements. In the case of UML there are some ongoing research activities to extend it for dealing with such kind of data for real-time and high-assurance systems, but the current published standard proposals have their tight limitations. We have specified a language extending the UML to support stochastic modelling, performance and dependability analysis and modelling of hardware and software systems.
Abstract: The design process of complex systems requires a precise checking of the functional and dependability attributes of the target design. The growing complexity of systems necessitates the use of formal methods, as the exhaustiveness of checks performed by the traditional simulation based testing is insufficient. For this reason, the mathematical models of various formal verification tools are planned to be automatically derived from UML-diagrams of the model by mathematical transformations guaranteeing a complete consistency between the target design and the input to the verification and validation tools. In the current paper, a general framework for an automated model transformation system is presented. The method starts from a uniform visual description and a formal proof concept of the particular transformations by integrating the powerful computational paradigm of graph transformation, planner algorithms of artificial intelligence, and deductive databases.
Keywords: system verification, graph transformation, model transformation, visual languages, planner algorithms, XMI, UML, dependability, verification, validation
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 UML-based metamodeling technique with precise static and dynamic semantics (based on a refinement calculus and graph transformation) where the structure and dynamic semantics of mathematical models can be defined in a UML notation without cumbersome mathematical formulae.
UML Statecharts are well-known visual means to capture the dynamic behavior of reactive systems in the object-oriented design methodology. Since the UML standard only contains an informal description on how to execute such statemachines mathematically precise semantic frameworks are required for an automated analysis. The current paper presents a formal semantics for UML statecharts based on a combination of metamodeling and graph transformation that is (i) simultaneously visual and precise, and (ii) clearly separates derived static concepts (like priorities, conflicts, etc.) from their dynamic interpretation thus scaling up well for different statechart variants (with, e.g., various priority strategies) and potential future changes in the standard.
As the Unified Modeling Language is evolving into a family of languages with individually specified semantics, there is an increasing need for highly automated and provenly correct model transformations that would assure the integration of local views of the system (in the form of different diagrams) into a consistent global view. Graph transformation provides an easy-to-understand visual specification technique to formally capture the rules of such transformations. In the paper, we summarize the concepts of VIATRA, the general purpose model transformation system together with the major correctness requirements and a model checking based verification method for model transformations.
Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture the operational semantics of modeling languages based on metamodeling techniques as demonstrated by benchmark applications focusing on the formal treatment of the Unified Modeling Language (UML). In the paper, we enable model checking-based symbolic verification for such modeling languages by providing a meta-level transformation of well-formed model instances into SAL specifications. We also discuss several optimizations in the translation process that makes our approach efficient and independent of the SAL framework.
In the paper, we propose an automated, SVG-based visualization framework for modeling languages defined by metamodeling techniques. Our framework combines XML standards with existing graph transformation and graph drawing technologies in order to provide an open, tool-independent architecture.
Model transformation systems are graph transformation systems that perform translations between languages defined by a corresponding metamodel as the type graph. The current paper proposes a reflective method for the automatic generation of the implementation for such transformation systems derived from a high--level specification consisting of a set of graph transformation rules and a control flow graph. The program generator takes a UML profile tailored to model transformation systems as the input, and produces the output Prolog program by successive model transformation steps. In this respect, only the core of the program generator is implemented by hand, and afterwards, this core provides automation for additional features of the VIATRA model transformation system.