A thorough system specification is insufficient to guarantee that a computer system will adequately perform its tasks during its entire life cycle. The early evaluation of system characteristics like dependability, correctness and performance is necessary to assess the conformance of the system under development to its targets. This paper presents the results achieved so far to develop an integrated environment, where design tools based on the UML (Unified Modeling Language) are augmented with validation and analysis techniques that provide useful information in the early phases of system design. Automatic transformations are defined for the generation of models to capture system behavioral properties, dependability and performance.
Abstract: Frequently the experimentation in the form of a post mortem analysis or fault injection experiment aim to reveal the correlation between some potential faults and the failure triggered by them. Note, that pattern sensitive failures are the most typical ones in software based systems. Therefore the analysis of complex systems must cope with a large population of system logs, where each individual pattern is large both in the terms of temporal duration, and in the number of signals and values to be recorded simultaneously. In the current paper we summarize our preliminary experiences for using data mining in the analysis phase of such error logs. The pilot experience was carried out on error logs from a Web server, however it must be pointed out, that a very similar approach based on the same technology can be useful in a variety of dependability-related fields as well, like fault injection based testing, stratified testing, etc.
Abstract: Diagnostics is one of the core problems in assuring the dependability of complex information technology systems. Nowadays diagnostics does not only a simple activity for identifying faulty hardware resources, but more and more it is a complex activity necessitating to cover both the hardware and software aspects. The increasing frequency of transient errors require more and more sophisticated diagnosis technologies, which also support the subsequent phases of fault handling as well, like damage confinement and reconfiguration. In practice, however one of the basic problems is the proper handling of the high complexity of the diagnostic process. One of the intrinsic assumptions behind all diagnostic algorithms is the notion of a maximum likelihood diagnosis. Frequently this assumption appears simply as "more faults occur with lower frequency than a few ones". Thus, the diagnostics aims at a minimal set of faulty elements compatible with the syndrome. Other approaches use an explicit notion of fault probabilities and assign different probabilities to different elements. In the present work, the diagnostics has been formulated as a maximization problem, moreover, it has been solved by state of the art technologies from the field of operations research.
Abstract: This paper describes methods and tools for automatic safety analysis of UML statechart specifications. Two types of analysis are presented. The first one checks completeness and consistency based on the static structure of the specification, thus it does not requires the generation of the reachability graph. Accordingly, this method scales up well to large systems. The second one performs dynamic analysis by checking safety related reachability properties with the help of a model checker. It is restricted to core critical parts of the system. Two approaches of the implementation of the static checking are discussed. The use of the tools is presented by a case study.
Abstract: The paper presents techniques that enable the modeling and analysis of redundancy schemes in distributed object-oriented systems. The replication manager, as core part of the redundancy scheme, is modeled by using UML statecharts. The flexibility of the statechart-based modeling, which includes event processing and state hierarchy, enables an easy and efficient modeling of replication strategies as well as repair and recovery policies. The statechart is transformed to a Petri-net based dependability model, which also incorporates the models of the replicated objects. By the analysis of the Petri-net model the designer can obtain reliability and availability measures that can be used in the early phases of the design to compare alternatives and find dependability bottlenecks. Our approach is illustrated by an example.
Abstract: The need for more and more dependable systems has been increased in the last decades. Strategic decisions during the design of these dependable systems require the joint control of the estimated cost and the product quality. Cost efficiency and development time became the most important factors of the software development process according to the international trends. The estimation of the cost remains a difficult problem till yet, despite of the use of standard, easy to understand modelling languages. On the other hand, no working environment is known supporting the gradually refined cost estimation derived automatically from the formal product models. In this paper the experiments of a pseudo cost estimation are detailed with a special emphasis on the cost estimation driven system design.
Abstract: This paper presents an overview of the results achieved in the framework of a project aiming at a commercial off the shelf (COTS) based, object-oriented design environment of UML-based process modeling and optimization. It reviews the de facto industry standards for Business Process Modeling (BPM) and mathematical problem definition and model exchange from the point of view of their applicability in modeling physical production processes.
Abstract: This paper describes methods and tools for automated safety analysis of UML statechart specifications. The general safety criteria described in the literature are reviewed and automated analysis techniques are proposed. The techniques based on OCL expressions and graph transformations are detailed and their limitations are discussed. To speed up the checker methods, a reduced form for UML statecharts is introduced. Using this form, the correctness and completeness of some checker methods can be proven. An example illustrates the application of the tools developed so far.
Abstract: This paper describes a design pattern for safety-critical user interfaces. This design is a version on of the Model-View-Controller architecture, but accepts safety and ergonomics criteria based on the literature.
Abstract: The current paper reports about an ongoing research to prove the correctness of designs described in UML. The most specific feature of the approach taken is the objective to prove the correct functioning of the target design even in the presence of faults anticipated in a predefined fault model.
Abstract: The design of complex, dependable systems requires a precise formal verification of design decisions during the system modelling phase. For that reason, the mathematical models of various formal verification tools are planned to be automatically derived from the system model described by UML-diagrams. In the current paper, a general framework for an automated model transformation system is outlined providing a uniform formal description method of such transformations by applying the powerful computational paradigm of graph transformation.
Keywords: formal verification, UML, model transformation.