Search

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.

Programmable logic controllers are typically programmed in one of the five languages defined in the IEC 61131 standard. While the ability to choose the appropriate language for each program unit may be an advantage for the developers, it poses a serious challenge to verification methods. In this paper we analyse and compare these languages to show that the ST programming language can efficiently and conveniently represent all PLC languages for formal verification purposes. Furthermore, we provide a translation method from IL to ST programming languages (for the Siemens implementation), together with a sketch of proof for its correctness. This allows the usage of the ST-based PLCverif model checking method for safety PLC programs.

The behavior of practical safety critical systems often combines real-time behavior with structured data flow. To ensure correctness of such systems, both aspects have to be modeled and formally verified. Time related behavior can be efficiently modeled and analyzed in terms of timed automata. At the same time, program verification techniques like abstract interpretation and software model checking can efficiently handle data flow. In this paper, we describe a simple formalism that represents both aspects of such systems in a uniform and explicit way, thus enables the combination of formal analysis methods for real-time systems and software using standard techniques.

Due to their distributed/parallel and data-driven nature, control systems can easily be modeled according to a data flow approach. Control systems are very often real-time systems; therefore, a formalism able to capture timing is required. In this paper we introduce a data flow model that includes time and priority for specifying real-time control systems and we give its formal semantics. The control system is specified by a data flow network which, beside the controller, may include the model of the plant at some abstraction level. Time is associated to any computational activity and time accounting is made directly in the model and not as a separate issue. Priorities allow to deal with events, as alarm signals, which cannot be delayed. A general framework for the indirect evaluation of the model is introduced, and a data flow network to timed Petri net transformation is defined allowing the utilization of the automatic tools of Petri nets for analyzing the temporal properties of the data flow network. The approach is illustrated by an example in which, after the application of the transformation, selected performance measures are computed. © 1998 Elsevier Science Ltd. All rights reserved.

This chapter provides an overview of the state of knowledge related to stochastic model-based assessment approaches, which are most commonly used for resiliency evaluation of current computing systems. The chapter first introduces a set of representative surveys developed in recent European projects, and then it provides a deeper description of common techniques used in model-based assessment of resilient systems. The most widely used modelling formalisms are reviewed, with a particular focus on state-based formalisms like Stochastic Petri Nets and its extensions. Techniques used in model construction and solution are also discussed, as well as the different classes of analysis tools and frameworks. The techniques analyzed in the chapter span from largeness avoidance and largeness tolerance techniques to more comprehensive modelling approaches that are integrated in the system’s development and assessment process. Some of these techniques try to cope with system’s complexity by automatically deriving the analysis models from engineering models like UML or AADL. Other approaches attack the complexity issue combining different evaluation methods, exploiting their possible complementarities and synergies. A discussion on the open research challenges in model-based resilience assessment is finally provided in the last part of the chapter, based on the reviewed techniques and on the activities carried out within the AMBER Coordination Action.

Robustness is an attribute of resilience that measures the behaviour of the system under non-standard conditions. Robustness is defined as the degree to which a system operates correctly in the presence of exceptional inputs or stressful environmental conditions. As triggering robustness faults could in the worst case scenario even crash the system, detecting this type of faults is of utmost importance. This chapter presents the state of the art on robustness testing by summarizing the evolution of basic robustness testing techniques, giving an overview of the specific methods and tools developed for major application domains, and introducing penetration testing, a specialization of robustness testing, which searches for security vulnerabilities. Finally, the use of testing results in resilience modelling and analysis is discussed.

System development processes are typically supported by dozens of different tools that assist the designer in various phases of development like modeling, verification, source code generation, testing. Tool-chains can be formed by the integration of tools that are related to the subsequent steps of the process. In this paper, we present a service-oriented, metamodel-driven, process-centric approach for the definition and execution of these tool-chains. Related data are handled as an important part of the process as the traceability of these is needed for the certification of the systems. The implementation is provided as an open, extensible framework. The approach is demonstrated using a model based test case generation process applied for automotive and railway systems.

A watchdog processor (WDP) is a relatively simple coprocessor built for concurrent, information compaction based error detection in the main program control flow. A new algorithm called SEIS (Signature Encoded Instruction Stream) is presented for assigning signatures to high level-instructions. The main idea of this method is to embed the information necessary to the program flow check into the signatures themselves, thus avoiding large reference databases in the WDP and allowing high operational speed. Solutions for a fault-tolerant multiprocessing and multi-tasking implementation are described as well.

The design of safety-critical systems and business-critical services necessitates to coordinate between a large variety of tools used in different phases of the development process. As certification frequently prescribes to achieve justified compliance with regulations of authorities, integrated tool chain should strictly adhere to the development process itself. In order to manage complexity, we follow a model-driven approach where the development process is captured using a precise domain-specific modeling language. Each individual step within this process is represented transparently as a service. Moreover, to carry out individual tasks, systems engineers are guided by semi-automated transformation steps and well-formedness constraint checking. Both of them are formalized by graph patterns and graph transformation rules as provided by the VIATRA2 framework. In our prototype implementation, we use the popular JBPM workflow engine as orchestration means between different design and verification tools. We also give some insights how this tool integration approach was applied in recent projects.

Current distributed mobile systems are usually characterized by a huge number of nodes, different network domains, different applications running, variability of the users' behavior, and dynamicity and heterogeneity of the communication networks. A typical example can be found in the automotive context, considering car-to-car and car-to-infrastructure communication scenarios. In this paper we propose a model-based approach for the dependability evaluation of distributed applications in a mobile environment. The final Multiple Phased System model representing the analyzed mobile scenario is automatically derived from high-level UML specifications through a sequence of model transformation steps. The evaluation workflow is based on i) a hierarchical modelling approach that analyzes the system at different levels, namely communication, architecture, application and user level; ii) a time-based system decomposition identifying different phases for different user activities and environment conditions.

In railway train-borne equipment, the Driver Machine Interface (DMI) acts like a bridge between the train driver and the onboard automatic train control system (European Vital Computer, EVC). While the DMI is required to operate in a critical context, current DMIs have no safety requirements. This implies that the EVC may automatically stop the train whenever the DMI is suspected to misbehave, leading to delay of the train, inconvenience for passengers and consequent possible profit loss. For these reasons a DMI with higher safety requirements is worth to be taken into account, even if it implies higher costs. The SAFEDMI European project aims at developing (i) a DMI at Safety Integrity Level 2 (SIL 2) using off-the-shelf components and a simple hardware architecture to reduce costs, and (ii) a SIL 2 wireless communication support for maintenance. This paper describes the architecture of a DMI which satisfies these objectives. The main hardware and software characteristics will be shown, including the proposed error detection techniques and the related fault handling (characterized by a new operational mode that allows DMI to restart silently, thus reducing unexpected train stops).

This workshop summary gives a brief overview of the workshop on ldquoResilience Assessment and Dependability Benchmarkingrdquo held in conjunction with the 38th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2008). The workshop aims at the presentation and exchange of ideas from the world wide research community and fostering discussions in order to give answers to the need for improving trustworthiness and understand the current risks inherent to computer systems and infrastructures. In particular the workshop aims at addressing key research challenges related to effective and accurate methods for measuring, assessing and benchmarking dependability and resilience.

Aspect-oriented modeling is proposed to design the architecture of fault tolerant systems. Notations are introduced that support the separate and modularized design of functional and dependability aspects in UML class diagrams. This notation designates sensitive parts of the architecture and selected architecture patterns that implement common redundancy techniques. A model weaver is presented that constructs both the integrated model of the system and the dependability model on the basis of the analysis sub-models attached to the architecture patterns. In this way fault tolerance mechanisms can be systematically analyzed when they are integrated into the system.

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.

Our paper introduces a runtime verification framework for concurrent monitoring of applications specified by UML statecharts. The approach offers a considerable 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 propositional linear temporal logic that fits to the advanced constructs of UML statecharts and an advanced watchdog scheme for concurrent supervision of program execution based on the statechart specification.

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.

This paper presents how the platform-specific development environment of time-triggered (TT) systems can be integrated with a visual design toolkit based on UML. The built-in facilities of UML and the modeling extensions introduced by us enable the unification of the advantages provided by both the embedded development environment and the UML tools. UML offers visual design, automatic code and documentation generation, while the underlying TT development environment offers platform-specific task and communication scheduling and fault tolerance middleware construction. This results in an integrated system that is capable of supporting the entire development within the framework of the UML tool

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, and (iv) several benchmark applications of the VIATRA framework.

The work in this paper is devoted to the definition of a dependability modeling and model based evaluation approach based on UML models. It is to be used in the early phases of the system design to capture system dependability attributes like reliability and availabiUty, thus providing guidelines for the choice among different architectural and design solutions. We show how structural UML diagrams can be processed to filter out the dependability related information and how a system-wide dependability model is constructed. Due to the modular construction, this model can be refined later as more detailed information becomes available. We discuss the model refinement based on the General Resource Model, an extension of UML. We show that the dependability model can be constructed automatically by using graph transformation techniques.

Signature based error detection techniques (e.g. the application of watchdog processors) can be easily extended to support software debugging. The run-time sequence of signatures is stored in an extension of the traditional checker. As the signatures identify the states of the program, a trace of the statements executed by the checked processor is available. The signature buffer can be efficiently utilized if the signature sequence is compressed. In the paper, two real-time compression methods are presented and compared. The general method uses predefined dictionaries, while the other one utilizes the structural information encoded in the signatures.

The paper presents techniques that enable the modeling and analysis of redundancy schemes in distributed object-oriented systems. The replication manager, as a 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.

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.

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.

Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of object-oriented systems. UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML Statechart Diagrams differ from classical statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.

A new control flow checking scheme, based on assigned-signature checking by a watchdog processor, is presented. This scheme is suitable for a multitasking, multiprocessor environment. The hardware overhead is comparatively low because of three reasons: first, hierarchically structured, the scheme uses only a single watchdog processor to monitor multiple processes or processors. Second, as an assigned-signature scheme it does not require monitoring the instruction bus of the processors. Third, the run-time and reference signatures are embedded into the checked program; thus, in the watchdog processor neither a reference database nor a time-consuming search and compare engine is required.

This paper proposes the application of On-Line Analytical Processing (OLAP) and data mining approaches to analyse the large amount of raw data collected in fault injection campaigns and dependability benchmarking experiments. We use data warehousing technologies to store raw results from different experiments in a multidimensional structure where raw data can be analysed by means of OLAP tools. Moreover, we present an approach for identifying the key infrastructural factors determining the behaviour of computer systems in the presence of faults by the application of data mining methods on the data sets. Results obtained with the proposed techniques identified important factors impacting performance and dependability that could not have been revealed solely by the benchmark measures.

In this paper we introduce an approach of aspect-oriented modelling and analysis of information systems. First we give an overview of the concepts of Aspect Oriented Programming and provide an outlook to model aspect-oriented programs. On the basis of this introduction, we describe a method of using aspects at the modelling level and weaving them into a single integrated model. Finally, we extend this framework with the automatic construction of analysis models based on separate aspect models. In our example, fault tolerance structures are modelled by aspects and the analysis model is a dependability model that is used to determine the non-functional properties of the system like reliability and availability. In this way the separate design of the functionality and the dependability is supported and the design decisions concerning fault tolerance can be analysed on the basis of the dependability model.

To enable the interoperability of high availability (HA) middleware systems the Service Availability Forum has released a set of open specifications. The benefit of having open specifications is the choice of implementations available from different vendors. When one chooses a product, one of the selection criteria (besides performance) is the robustness of the implementation, as the crashing or hanging of such a HA middleware causes the failure of the whole system. The challenge is to develop the appropriate technology for measuring and comparing robustness of HA middleware implementations. Based on our earlier results, we present a set of automatic testing tools and a benchmark suite constructed using these tools. We demonstrate the robustness testing approach by comparing the results of benchmarking carried out on three HA middleware implementations.

Model-driven engineering methodologies are often used for the design and integration of the software and hardware components in automated production systems. Architecture models in general purpose or domain specific modeling languages allow the modular and systematic construction of formal analysis models for the evaluation of dependability and performability. The on-line reconfiguration and fault handling actions in the system introduce changes in the architecture and parameters, and thus result in a multi-phased operation. We propose a mission automaton formalism to describe reconfigurations, fault handling and parameter changes over architecture models. By maintaining the architecture model, which is modified by the reconfigurations, along with the corresponding analysis models, a stochastic phased-mission system (PMS) is obtained and solved for dependability.

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-priori 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.