تجزیه و تحلیل سیستم مبتنی بر مدل با استفاده از چی و اوپال: مطالعه موردی صنعتی

New methods and techniques are needed to reduce the integration and test effort (lead time, costs, resources) in the development of high-tech multi-disciplinary systems. To facilitate this effort reduction, a method called model-based integration and testing is being developed. The method allows to integrate formal and executable models of system components that are not yet physically realized with available realizations of other components. The combination of models and realizations is then used for early analysis of the integrated system by means of validation, verification, and testing. The analysis enables early detection and prevention of problems that would otherwise occur during real integration, resulting in a significant reduction of effort invested in the real integration and testing phases. This paper illustrates the application of the method to a realistic industrial case study, focusing on verification of the models obtained. We show how a system model has been developed for model-based integration and testing in the timed process algebra χχ (Chi), and how certain behavioral properties of this model have been verified by the Uppaal model checker.

High-tech multi-disciplinary systems like wafer scanners, electronic microscopes and high-speed printers are becoming more complex every day. Growing system complexity also increases the effort (in terms of lead time, cost, resources) needed for the, so-called, integration and testing phases. During these phases, the system is integrated by combining component realizations and, subsequently, tested against the system requirements. Existing industrial practice shows that the main effort of system development is shifting from the design and implementation phases to the system integration and testing phases [1]. Furthermore, finding and fixing problems during integration and testing can be up to 100 times more expensive than finding and fixing the problems during the requirements and design phases [2]. Literature reports wealth of research proposing a model-based way of working to counter the increase of development effort, like requirements modeling [3], model-based design [4], model-based code generation [5], hardware–software co-simulation [6], and model-based testing [7]. In most cases, however, these model-based techniques are investigated in isolation, and little work is reported on combining these techniques into an overall method. Although model-based systems engineering [8] and OMG’s model-driven architecture [9] (for software only systems) are such overall model-based methods, these methods are mainly focusing on the requirements, design, and implementation phases, rather than on the integration and test phases. Furthermore, literature barely mentions realistic industrial applications of such methods, at least not for high-tech multi-disciplinary systems. Our research within the TANGRAM project [10] focusses on a method of model-based integration and testing (MBI&T), introduced in [11]. In this method, formal executable models of system components (e.g. software, mechanics, electronics) that are not yet realized are integrated with available realizations of other components, establishing a model-based integrated system. Such a model-based integrated system can be established much earlier compared to a real integrated system, and it can effectively be used for early model-based system analysis and system testing, which has three main advantages. First, the fact that it is earlier means that the integration and test effort is distributed over a wider time frame. This reduces the effort to be invested during the real integration and testing phases. Second, it allows earlier and thus cheaper detection and prevention of problems that would otherwise occur during real integration. Early problem detection and prevention also reduces the corresponding diagnostic and fix effort and increases the quality of the system at an earlier stage. Finally, the use of formal models enables the application of powerful model-based analysis techniques, like simulation and verification. These analysis techniques help to improve the insight in the system’s behavior for the engineers, resulting in better system quality as well. This paper illustrates the application of the MBI&T method to the development of a part of a realistic industrial system, namely the ASML [12] wafer scanner. In the case study, a system is formally specified by means of a process algebraic language χχ (Chi) [13]. The χχ language is supported by a toolset that allows simulation of the obtained χχ model, e.g. for the analysis of system performance and exceptional behavior handling. The formal semantics of χχ enable functional analysis of χχ models, e.g. verification of the correctness of a system model. Combining performance analysis and functional analysis in the χχ environment is the objective of the TIPSy project [14]. As a part of this project, a translation scheme [15] from χχ to Uppaal timed automata [16] and [17] has been developed and integrated into the χχ toolset, allowing verification of the translated models by the Uppaal model checker. The Uppaal tool has been used in a number of industrial case studies. A complete overview can be found in [18]. Mostly, the case studies concerned verifying real-time controllers [19] and communication protocols [20], [21], [22] and [23]. In [24] the problem of synthesizing production schedules and control programs for the mock-up of the batch production plant was addressed. In [25] the throughput of an ASML wafer scanner was analyzed with Uppaal. The case study described in this paper focuses on verification of system properties such as deadlock freeness, liveness, safety, and temporal properties using the χχ to Uppaal translation scheme and the Uppaal model checker. The goal of the case study and this paper is threefold. We show the potential of the proposed MBI&T method (in which the verification techniques are used) to reduce the integration and test effort of industrial systems. We investigate the applicability and usability of the χχ toolset as integrated tool support for all aspects of the MBI&T method, particularly focusing on the implementation of the χχ to Uppaal translation scheme. Finally, we discuss the advantages, applicability, and scalability of verification techniques for realistic industrial systems. The structure of the paper is as follows. Section 2 describes the MBI&T method in general with the focus on the use of verification within the method. Section 3 introduces the industrial case study to which the MBI&T method has been applied. The activities that have been performed in the case study are described in Sections 4 (modeling and simulation with χχ) and 5 (translation to and verification with Uppaal). Although model-based and real system testing are not the focus of this paper, Section 6 gives a short summary of these steps. Finally, the conclusions are drawn and discussed in Section 7.

The goal of the case study and this paper was threefold: (1) to show the potential of the proposed MBI&T method (in which the verification techniques are used) to reduce the integration and test effort of industrial systems; (2) to investigate the applicability and usability of the χχ toolset as integrated tool support for all aspects of the MBI&T method, particularly focusing on the translator from χχ to Uppaal; (3) to discuss the advantages, applicability, and scalability of verification techniques for realistic industrial systems. Application of the MBI&T method (and verification as its part) proved to be successful for the realistic industrial case study, showing relevant advantages for the system development process. First, the modeling activities helped to clarify, correct, and complete the design documentation. By simulation and verification, a number of design and integration errors were detected and fixed earlier and cheaper when compared to current system development. Finally, a part of the model was integrated with a realized component to enable early, fast, and cheap model-based system testing. Again, multiple errors in realization were detected and fixed, saving significant amounts of time and rework during the real integration and test phases. This clearly shows the applicability and value of the MBI&T method for industrial system development. In total, five errors were found by simulation and verification of the system model. Three of these errors were design errors; only one of them was discovered by means of simulation. The other two design errors, discovered by verification only, both concern the non-deterministic behavior of parallel processes. This is difficult, if not impossible, to understand and to analyze by simulation or by reviewing the design documentation. This illustrates that verification should be used for designing real industrial systems, which often involve both high-level parallelism and non-deterministic behavior. The other two errors were modeling errors introduced in the modeling and model transformation step. To prevent model transformation errors, the translation scheme from χχ to Uppaal should be extended with the scope operator and process instantiation. With these extensions, the translation scheme is well suited for translating most χχ models. Unfortunately, the guarded delay and nested parallelism cannot be translated in the general case and these constructs should be avoided while modeling; otherwise they have to be transformed manually. The χχ toolset, extended with the Uppaal translator, is suitable for all activities of the MBI&T method: modeling, simulation, verification, component testing, model-based integration and integrated system testing. The system aspects that were modeled in the case study (supervisory machine control in software, interrupt behavior, electronic communication) can easily be modeled in χχ. The fact that the biggest state space generated for our system is rather small (order 20,000 states) indicates that the approach is applicable to similar size or even more complex industrial systems. However, giving quantitative statements on the scalability of this approach is difficult. The Uppaal model checker verifies the properties by generating the symbolic state space on-the-fly. This means that it does not need to generate the entire state space to verify a property, resulting in a significant reduction of the needed amount of time and memory. However, the size of the generated state space is, then, dependent on the property to be verified. Furthermore, the size of the state space heavily depends on the model itself, for instance, the number of automata, clocks, and variables, the level of non-determinism, and the structure of the automata. This is also recognized in literature, for example in [36], in which a medium sized rather detailed and deterministic model with six processes could easily be handled, while the analysis of a small example with high non-determinism failed. The state space size is also influenced by model checker options, such as depth-first or breadth-first search, etc. This means that predicting the size of the state space, and thus making statements on the scalability of the approach, is difficult. Our system contains 8 rather deterministic automata with 5 clocks and 29 variables, and the amount of memory used during model checking was just under 1 MB. Note that this memory was used not only for storing the state space, but also for execution of the model checker itself. In literature, the sizes of the verification problems are indicated in different terms. Some examples from literature mention applications with characteristics like 11 automata [22] and [23], 9 clocks and 28 variables [37], 16 automata, 4 clocks, and 32 variables [21], up to 125 automata with 183 clocks [24] and 100 (equivalent) automata with a state space in the order of 700,000 states [38], and applications with memory usage from several hundreds of MB’s [21], [24] and [39] up to 3 GB [37]. Although no general quantitative statement on scalability can be given, this paper shows that verification is a relevant analysis technique to find problems in industrial systems and that the limits of verification were not reached in the case study. For verification of more complex systems, the potential state space explosion problem remains the main obstacle. However, the size of problems that can be handled increases due to continuous research work and tool improvements, as we also experienced in the case study when upgrading to a newer version of Uppaal. For example, the state space size of models can be optimized by using meta-variables [23] or by a recently developed symmetry reduction technique [38]. Furthermore, several options are available for state space optimization, state space approximation and efficient data storage [37]. Besides the development of techniques to reduce the state space and memory usage, the computing power available for verification also increases continuously, with faster processors, more memory, and distributed computing techniques [40]. All these techniques provide a wide range of verification solutions to tackle problems of different types and sizes, as shown in [18], [19], [20], [21], [22], [23], [24] and [25].