IEEE Industrial Electronics Society
IEEE Industrial Electronics Society
View PDF version
Access this issue at IEEEXplorer
Guest Editorial: Special Section on Formal Methods in Manufacturing
Javier Campos
1. Observability of Switched Linear Systems
David Gómez-Gutiérrez, Guillermo Ramírez-Prado, Antonio Ramírez-Treviño, and José Ruiz-León
Abstract: This work deals with finite time observability of Switched Linear Systems (SLS) when they are represented by a family of non autonomous Linear Systems (LS) and an Interpreted Petri Net (IPN). Based on this SLS representation, new detection of the commutation time and LS distinguishability characterizations in SLS extended to the non autonomous case are presented. Using these results, the novel concept of distinguishability between LS sequences is presented and characterized. This concept together with the IPN input-output information is used to determine the IPN marking sequence. From the knowledge of this sequence, the conditions for the computation of the continuous state are presented. Also necessary and sufficient conditions for the observability in infinitesimal time are provided.
2. On Formal Analysis of IEC 61499 Applications, Part A: Modeling,
Goran Cengic and Knut Åkesson
Abstract: IEC 61499 is a standard architecture, based on function blocks, for developing distributed control and measurement applications. However, the standard has no formal semantics and different interpretations of the standard have emerged. As a consequence it is harder to transfer applications between different standard compliant platforms. This paper presents a formal framework for mathematical modeling and comparison of different execution semantics. The framework provides definitions that allow modeling of applications and execution semantics separately. Together, the models can be used to analyze and compare how an application would behave when executed using different execution semantics. In addition, a mathematical model made possible by the framework has been used as a basis for implementation of a runtime environment that can execute applications and a software tool that generates formal models suitable for formal verification, both assuming different execution semantics.
3. On Formal Analysis of IEC 61499 Applications, Part B: Execution Semantics
Goran Cengic and Knut Åkesson
Abstract: IEC 61499 is a standard architecture, based on function blocks, for developing distributed control and measurement applications. However, the standard has no formal semantics and different interpretations of the standard have emerged. As a consequence, the execution behavior of applications running on different platforms may exhibit different behavior, thus making it harder to transfer applications between the platforms. This paper shows how three different execution semantics, BSEM, NPMTR, and CBEM can be mathematically defined. The mathematical definitions can be used to analyze an application's behavior when executed using those execution semantics. The mathematical definitions have been used as a basis for implementation of a runtime environment and a software tool that generates formal models suitable for formal verification. Formal verification can be used to help discover execution errors before the application is executed on the factory floor.
4. Refactoring of Execution Control Charts in Basic Function Blocks of the IEC 61499 Standard
Valeriy Vyatkin and Victor Dubinin
Abstract: This paper deals with refactoring of execution control charts of IEC 61499 basic function blocks as a means to improve the engineering support potential of the standard in development of industrial control applications. The main purpose of the refactoring is removal of arcs without event inputs. Extended refactoring, proposed in the paper, also helps to get rid of potential deadlock states. The ECC refactoring is implemented as a set of graph transformation rules. A prototype has been implemented using the AGG software tool. The refactoring can help in implementing equivalent transformation of control programs without introducing errors.
5. Modeling Distributed Transportation Systems Composed of Flexible Automated Guided Vehicles in Flexible Manufacturing Systems
David Herrero-Pérez and Humberto Martínez-Barberá
Abstract: This paper proposes a methodology for modeling and controlling a flexible material handling system (MHS), composed of multiple automated guided vehicles (AGVs), suitable for Flexible Manufacturing Systems (FMSs). The AGVs incorporate artificial intelligent techniques to i) facilitate the configuration and adaptation when there are layout modifications and ii) simplify the interaction between them using simple coordination models. In order to achieve higher flexibility, the MHS makes use of a decentralized navigation control, which increases autonomy and scalability, and a distributed Petri net for solving task allocation and traffic control problems. In order to facilitate the integration with the manufacturing processes, tasks dispatched by manufacturing cells are allocated by the MHS itself, taking into account pending transportation tasks and the system's performance. The whole system has been tested in a real factory and is currently in operational use.
6. Ensuring Correctness in the Specification and Handling of Non-Functional Attributes in High-Integrity Real-Time Embedded Systems
Cancila, Daniela (contact); Passerone, Roberto; Vardanega, Tullio; Panunzio, Marco
Abstract: In high-integrity systems, the focus of the development process is geared to assuring that the assertions made on the system are both correct (i.e., semantically sustainable) and feasible (i.e., true at run time). Some of those assertions take effect in the non-functional domain, that is, in how the system is realized and behaves in time, space and communication during execution; others in the functional domain, and thus concern what outputs the system produces for its inputs. In this paper we address the problem of achieving correct specification and handling of non-functional attributes, with particular regard to the concurrent structure of the system, the safeness of the interaction protocols engaged in it, and the guarantee that its timing feasibility can be statically verified. Our approach is based on a Model-Driven Engineering methodology, in which correctness can be ensured by construction or verified at a high level of abstraction, while the run-time implementation structure and code are automatically generated. We employ the Ravenscar Computation Model (RCM) and focus in particular on aerospace applications, which impose stringent requirements on correctness properties. We discuss an algebraic formalization of our model based on graph theory which we use to prove safe termination in systems compliant with RCM, and show how to use the MAST+ static analyzer to verify the timing aspects. We finally illustrate the results of a prototype tool that was developed for evaluation by major industrial players in the European space industry.
7. Component-Based Safety Analysis of FPGAs
Conmy, Philippa (contact); Bate, Iain
Abstract: Component-based and modular software development techniques have become established in recent years. Without complementary verification and certification methods the benefits of these development techniques are reduced. As part of certification, it is necessary to show a system is acceptably safe which subsumes both the normal and abnormal (failure) cases. However, non-functional properties, such as safety and failures, are abstraction breakers, cutting across multiple components. Also, much of the work on component-based engineering has been applied to software-based systems rather than FPGA-based systems whose use is becoming more popular in industry. In this paper we show how a modular design embedded on a FPGA can be exhaustively analysed (from a safety perspective) to derive the failure and safety properties to give the evidence needed for a safety case. The specific challenges faced are analysing the fault characteristics of individual electronic components, combining the results across software modules, and then feeding this into a system safety case. A secondary benefit of taking this approach is that there is less uncertainty in the performance of the device, hence, it can be used for higher integrity systems. Finally, design improvements can be specifically targeted at areas of safety concern, leading to more optimal utilisation of the FPGA device.
8. Improving Fault Tolerance in High-Precision Clock Synchronization
Gaderer, Georg; Loschmidt, Patrick; Sauter, Thilo
Abstract: The very popular Precision Time Protocol (PTP or IEEE 1588) is widely used to synchronize distributed systems with high precision. The underlying principle is a master/slave concept based on the regular exchange of synchronization messages. This paper investigates an approach to enhance PTP with fault tolerance and to overcome the transient deterioration of synchronization accuracy during a recovery from a master failure. To this end, a concept is proposed where a group of masters negotiates a fault-tolerant agreement on the system-wide time and transparently synchronizes the associated IEEE 1588 slaves. Experimental verification on the basis of an Ethernet implementation shows that the approach is feasible and indeed improves the overall synchronization accuracy in terms of fault tolerance.
9. Multi-Zone Thermal Processing in Semiconductor Manufacturing: Bias Estimation
Ling, Keck Voon; Yan, Han; Ho, Weng Khuen; Lim, Khiang Wee
Abstract: Temperature uniformities within a wafer and from wafer to wafer have significant impact on the smallest feature size or critical dimension of integrated circuits. These are important issues with stringent specifications. To obtain temperature uniformity, a wafer is heated by multiple independently controlled heating elements simultaneously. The accuracy of temperature sensing is hence an important issue. In this paper, sensor bias is estimated for the difficult problem where measurement outliers are close to good data such that they cannot be separated easily. Equations are derived to predict the variance of the estimates from sample size. This information enables the selection of an efficient estimator. Sensor bias estimation efficiency translates into earlier bias removal and less faulty wafers. The theory is verified experimentally in a multi-zone thermal system for semiconductor wafer processing.
10. An EWMA algorithm with a cycled resetting (CR) discount factor for drift and fault of high-mix Run-To-Run Control
Zheng, Ying (contact); Ai, Bing; Wong, David; Jang, Shi-Shang; Zhang, Jie; Wang, Yanwei
Abstract: Run-to-run controllers based on the exponential weighted moving average (EWMA) statistic are probably the most frequently used for the quality control of certain semiconductor manufacturing process steps. The threaded-EWMA run-to-run control is an important stable control scheme. However, the process out-puts will deviate largely in the first few runs of each cycle if the disturbance follows an IMA(1,1) series with deterministic linear drift and the thread has a long break length. In this paper, the output of the threaded-EWMA run-to-run control is derived, stability conditions are given, and the causes of large deviations in the first few runs of each cycle are found. Based on the analysis of system performance, a cycled re-setting (CR) algorithm for discount factor is proposed to reduce the large deviations as well as to achieve the minimum asymptotic variance control. Furthermore, how to deal with step fault is also discussed in this paper. By analyzing the influence of the fault, a discount factor resetting fault-tolerant (RFT) approach is proposed. Simulation study shows both the mean square error (MSE) and variance of the output by the proposed algorithm is about 30% to 50% lower than that of the algorithm with fixed discount factor in the process with and without oscillation. This verifies the effectiveness of the proposed approach.
11. Inspiring Innovative Design Integration by Collaborative Exploration of Boolean Operations
Yang Zheng, Haifeng Shen, and Chengzheng Sun
Main Page Site Search Welcome About F.A.Q. Awards Nominate History Legal Members Officers AdCom Minutes Committees Technical Education Ind. Forum Council Lecturers Volunteers Chapters Students Publications Trans on IE Trans on II Magazine Newsletter Photographs Conferences IECON ETFA ICIT INDIN ISIE Standards Treasurer Logos/links W&I Web Editor Wikipedia
