检索结果-内蒙古大学图书馆

function block diagram to UPPAAL Timed Automata Transformation Based on Formal Models

IFAC Proceedings Volumes 2012年第6期45卷 1653-1659页

作者： Doaa Soliman Kleanthis Thramboulidis Georg Frey Saarland University Saarbrücken Germany University of Patras Greece

Verification of IEC61131-3 based safety applications is a challenge in the development process of industrial systems. In this paper, we formally describe the set of transformation rules we have defined for the automatic transformation of IEC61131-3 function block based safety applications to UPPAAL timed automata models. These models are used for the verification of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the formal definition of the transformation rules. We adopted as format of the source models the PLCopen XML specification that is widely accepted by industry. Based on this format and the defined transformation rules a prototype model transformer was developed using Java. The transformer was used on several safety applications to check its functionality and the efficiency of the transformation process.

关键词： IEC61131-3 UPPAAL function block diagram Safety Applications PLCopen

来源：评论

学校读者我要写书评

暂无评论

Automated Test Coverage Measurement for Reactor Protection System Software Implemented in function block diagram

Automated Test Coverage Measurement for Reactor Protection S...

引用

29th International Conference on Computer Safety, Reliability and Security

作者： Jee, Eunkyoung Kim, Suin Cha, Sungdeok Lee, Insup Univ Penn 3330 Walnut St Philadelphia PA 19104 USA Korea Adv Inst Sci & Technol Daejeon South Korea Korea Univ Seoul South Korea

ISBN: (纸本)9783642156502

We present FBDTestMeasurer, an automated test coverage measurement tool for function block diagram (FBD) programs which are increasingly used in implementing safety critical systems such as nuclear reactor protection systems. We have defined new structural test coverage criteria for FBD programs in which dataflow-centric characteristics of FBD programs were well reflected. Given an FBD program and a set of test cases, FBDTestMeasurer produces test coverage score and uncovered test requirements with respect to the selected coverage criteria. Visual representation of uncovered data paths enables testers to easily identify which parts of the program need to be tested further. We found many aspects of the FBD logic that were not tested sufficiently when conducting a case study using test cases prepared by domain experts for reactor protection system software. Domain experts found this technique and tool highly intuitive and useful to measure the adequacy of FBD testing and generate additional test cases.

关键词： test coverage measurement test automation function block diagram programmable logic controller

来源：评论

学校读者我要写书评

暂无评论

Automated Test Sequence Generation for function block diagram Programs 23

Automated Test Sequence Generation for Function Block Diagra...

引用

23rd Asia-Pacific Software Engineering Conference (APSEC)

作者： Song, Jiyoung Jee, Eunkyoung Bae, Doo-Hwan Korea Adv Inst Sci & Technol Sch Comp Daejeon South Korea

ISBN: (纸本)9781509055753

As function block diagram (FBD) programs are used to implement safety-critical systems such as nuclear reactor protection systems, it is crucial to be able to generate effective test cases. The FBD is one of programming languages that are used for programmable logic controllers (PLCs). PLC programs are repeatedly run within a particular scan time for every execution. Among the constituents of FBD programs, function blocks and feedback variables use the inputs and outputs of the previous scan cycle on which to operate. Researchers have recently developed an automated test generation technique that satisfied several structural test coverage criteria for FBD programs using symbolic execution. However, their work could not generate test sequences for consecutive scan cycle but test inputs for one scan cycle. Test sequences are essential for testing FBD programs that have function blocks and feedback variables. This paper extends previous work in the field by generating test sequences for FBD programs with function blocks in a fully automated manner. The key technique involves explicitly unwinding FBD programs and solving test requirements using an SMT solver. We conduct experiments on increasing the coverage of test requirements by unwinding cycles and evaluating the effectiveness of the test set using mutation analysis with several subject programs, including a real-world reactor protection system. The experimental results show that the proposed approach is able to generate effective test sequences for FBD programs.

关键词： function block diagram automated test sequence generation structural testing

来源：评论

学校读者我要写书评

暂无评论

Sequential function Chart to function block diagram Transformation with Explicit State Representation 40th

Sequential Function Chart to Function Block Diagram Transfor...

引用

40th Anniversary International Conference on Information Systems Architecture and Technology (ISAT)

作者： Hojda, Maciej Filcek, Grzegorz Popek, Grzegorz Wroclaw Univ Sci & Technol Fac Comp Sci & Management Ignacego Lukasiewicza 5 PL-50371 Wroclaw Poland

ISBN: (纸本)9783030306045;9783030306038

This paper presents a method and a tool for converting Sequential function Charts into function block diagrams in a manner that models states with the use of flip-flops. Order of evaluation is enforced through the use of explicit delays. Presented approach can be used when SFC programming is not directly available but the developer wants to use advantages of SFC modeling.

关键词： Sequential function Chart function block diagram Programmable Logic Controller

来源：评论

学校读者我要写书评

暂无评论

Test case generation for function block diagram based on blocks' predefined behaviour 23

Test case generation for Function Block Diagram based on blo...

引用

23rd International Conference on Process Control (PC)

作者： Ausberger, Tomas Kubicek, Karel Medvecova, Pavla Myslivec, Tomas Univ West Bohemia NTIS New Technol Informat Soc Fac Appl Sci Tech 8 Plzen 30614 Czech Republic

ISBN: (纸本)9781665403306

Automatic test case generation based on knowledge of a model is currently a challenge for many researchers and developers. This article describes the first of two complementary methods for test case generation for function block diagram (FBD) models and grey-box testing. The first method utilises predefined tested behaviour (unit tests) of each used function block and combines them together. This method adds a structural limitation to the model. Therefore, the model needs to be split into multiple parts and processed per partes. The second method is then used for a combination of these partial results. Together these two methods can generate test cases even for models that include feedbacks, internal states, and traffic delays.

关键词： automatic tests function block diagram structure-based testing test case generation verification unit test model checking

来源：评论

学校读者我要写书评

暂无评论

FBDVerifier: Interactive and Visual Analysis of Counter-example in Formal Verification of function block diagram

引用

JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY 2010年第3期42卷 171-188页

作者： Jee, Eunkyoung Jeon, Seungjae Cha, Sungdeok Koh, Kwangyong Yoo, Junbeom Park, Geeyong Seong, Poonghyun Korea Univ Dept Comp Sci & Engn Coll Informat & Communict Seoul South Korea Korea Univ CEEDS Seoul South Korea Korea Adv Inst Sci & Technol Div Comp Sci Taejon South Korea Samsung Elect Co Ltd Seoul South Korea Korea Adv Inst Sci & Technol Dept Nucl & Quantum Engn Taejon South Korea Konkuk Univ Div Comp Sci & Engn Dept Comp Sci & Engn Seoul South Korea Korea Atom Energy Res Inst I&C & Human Factors Ctr Instrumentat & Control & Human Factors Div Taejon South Korea

Model checking is often applied to verify safety-critical software implemented in programmable logic controller (PLC) language such as a function block diagram (FBD). Counter-examples generated by a model checker are often too lengthy and complex to analyze. This paper describes the FBDVerifier which allows domain experts to perform automated model checking and intuitive visual analysis of counter-examples without having to know technical details on temporal logic or the model checker. Once the FBD program is automatically translated into a semantically equivalent Verilog model and model checking is performed using SMV, users can enter various expressions to investigate why verification of certain properties failed. When applied to FBD programs implementing a shutdown system for a nuclear power plant, domain engineers were able to perform effective FBD verification and detect logical errors in the FBD design.

关键词： function block diagram Formal Verification Counter-example Visualization Verilog Translation Programmable Logic Controller Model Checking

来源：评论

学校读者我要写书评

暂无评论

functionally-Equivalent Formalization and Automated Model Checking of function block diagrams

引用

IEEE ACCESS 2025年 13卷 22197-22229页

作者： Ausberger, Tomas Kubicek, Karel Medvedcova, Pavla Univ West Bohemia Pilsen Fac Appl Sci New Technol Informat Soc NTIS Plzen 30100 Czech Republic

In the development and verification of safety-critical and safety-related Instrumentation and Control (I&C) systems, it is essential to ensure there is no deviation from the requirements of the assignment during development. Model checking is a method of formal verification which can be used to prove whether a formal model satisfies its formal requirement. Since algorithms of I&C systems are generally informal, they can not be verified by model checking directly, but they must be carefully translated. This article presents a new method based on functionally-equivalent formalisation and model checking. This method can be used for automatic verification of I&C algorithms by model checking while preserving obtained proofs from a formalised model in the original algorithm. There are several problems associated with the verification of PLCs by model checking: 1) State space explosion, 2) Model consistency, 3) Specifying Properties to be Checked, 4) Representing PLC execution cycle, 5) TONs timers representation. This aims of this article is to address points 1), 2), 4) and 5). The article also presents conditions for implementing these algorithms in a target I&C system under which the obtained proofs can also be expected in the physical I&C system. This article primarily focuses on formalisation and model checking of function block diagram (FBD) algorithms. However, the presented methods can also be extended to other programming languages.

关键词： Model checking Safety Computational modeling Standards Formal verification IEC Standards Software algorithms Mathematical models Explosions Software Formal model formal verification function block diagram FBD functionally-equivalent formalization Formalization IEC standards instrumentation and control (I&C) systems model checking safety-critical system safety-related system verification process

来源：评论

学校读者我要写书评

暂无评论

Software safety analysis of function block diagrams using fault trees

引用

RELIABILITY ENGINEERING & SYSTEM SAFETY 2005年第3期88卷 215-228页

作者： Oh, Y Yoo, J Cha, S Son, HS Korea Adv Inst Sci & Technol Dept Elect Engn & Comp Sci Taejon 305701 South Korea IIRTRC SPIC AITrc Taejon 305701 South Korea Korea Atom Energy Res Inst I&C & HF Team Taejon South Korea

As programmable logic controllers (PLCs) are often used to implement safety-critical embedded software, safety demonstration of PLC code is needed. In this paper, we propose a fault tree analysis technique on function block diagrams (FBDs) which is one of the most widely used PLC programming languages. FBD is currently being used to develop Reactor Protection System (RPS) for a nuclear power plant in South Korea. Our approach to fault tree analysis, which combines fault-oriented and cause/effect-oriented viewpoints, is easy to understand and offers systematic guidelines to ensure safety of PLC code. Domain experts found the approach to be useful through a case study on RPS, and this paper compares completeness and comprehensiveness of the semi-automatically generated fault trees using the proposed approach against the one manually prepared by nuclear safety engineers. (c) 2004 Elsevier Ltd. All rights reserved.

关键词： safety analysis fault tree analysis function block diagram programmable logic controller

来源：评论

学校读者我要写书评

暂无评论

Transformation of function block diagrams to UPPAAL timed automata for the verification of safety applications

引用

ANNUAL REVIEWS IN CONTROL 2012年第2期36卷 338-345页

作者： Soliman, Doaa Thramboulidis, Kleanthis Frey, Georg Univ Saarland Chair Automat D-66123 Saarbrucken Germany Univ Patras GR-26110 Patras Greece

Verification of IEC 61131-3 based safety applications is a challenge in the industrial automation domain. In this paper, the transformation of FBD diagrams to UPPAAL formal models was adopted to address this challenge. A set of transformation rules are defined for the automatic transformation of IEC 61131-3 function block based safety applications to UPPAAL timed automata models. These models are next used for the verification of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the definition of the transformation rules. Based on this a prototype model transformer was developed using Java. The transformer was used with various safety applications to check the efficiency of the transformation process. A laboratory system is presented as a case study to highlight the proposed approach. (C) 2012 Elsevier Ltd. All rights reserved.

关键词： function block diagram Timed automata IEC 61131-3 UPPAAL Verification Safety applications PLCopen

来源：评论

学校读者我要写书评

暂无评论

Model-Based Test Suite Generation for function block diagrams using the UPPAAL Model Checker

Model-Based Test Suite Generation for Function Block Diagram...

引用

6th IEEE International Conference on Software Testing, Verification and Validation (ICST)

作者： Enoiu, Eduard Paul Sundmark, Daniel Pettersson, Paul Malardalen Univ Malardalen Real Time Res Ctr MRTC Vasteras Sweden

ISBN: (纸本)9780769549934;9781479913244

A method for model-based test generation of safety-critical embedded applications using Programmable Logic Controllers and implemented in a programming language such as function block diagram (FBD) is described. The FBD component model is based on the IEC 1131 standard and it is used primarily for embedded systems, in which timeliness is an important property to be tested. Our method involves the transformation of FBD programs with timed annotations into timed automata models which are used to automatically generate test suites. Specifically we demonstrate how to use model transformation for formalization and model-checking of FBD programs using the UPPAAL tool. Many benefits emerge from this method, including the ability to automatically generate test suites from a formal model in order to ensure compliance to strict quality requirements including unit testing and specific coverage measurements. The approach is experimentally assessed on a train control system in terms of consumed resources.

关键词： function block diagram plc model-based testing timed automata test-suite generation structural coverage

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：