Formal syntax and semantics of basic function blocks in IEC 61499

The use IEC 61499 (International Electrotechnical Commission, IEC) as a modelling language for distributed industrial process measurement control systems lacks formal syntax and explicit semantics and can hardly ensure reliability and validity of systems. As the basic modelling elements in IEC 61499, syntax and semantics of basic function block (BFB) are specified informally and ambiguously. Hence, the formal syntax and explicit semantics of BFB are advanced to achieve the behavioural consistency and correct results, in this article. The formal syntax is defined by mathematical set theory and the explicit semantics are composed of two kinds of semantics: denotational and execution semantics. The denotational semantics explain the meaning of language with an extended Mealy finite-state machines for the formal verification in a formal way. The execution semantics provide execution rule and algorithm scheduling in the execution process and involve an input machine and the main part, in which input machine masters the matching relation of event and data input variables and the main part offers execution orders and algorithm computation. Besides, the execution semantics of BFB are exemplified with two events and algorithms as the execution order t1–t20, and a flowchart of BFB behaviours is given as an overview of the processing steps for implementation or code generation.

Download Full-text

Enhanced IEC 61499 system model for evolution of control applications in distributed Industrial-Process Measurement and Control Systems

2007 European Control Conference (ECC) ◽

10.23919/ecc.2007.7068501 ◽

2007 ◽

Author(s):

Thomas Strasser ◽

Christoph Sunder ◽

Martijn N. Rooker ◽

Oliver Hummer ◽

Alois Zoitl ◽

...

Keyword(s):

Control Systems ◽

Industrial Process ◽

System Model ◽

Control Applications ◽

Process Measurement ◽

And Control ◽

Measurement And Control ◽

Iec 61499

Download Full-text

Refactoring of Execution Control Charts in Basic Function Blocks of the IEC 61499 Standard

13th IFAC Symposium on Information Control Problems in Manufacturing ◽

10.3182/20090603-3-ru-2001.00030 ◽

2009 ◽

Author(s):

Dubinin, Victor

Keyword(s):

Control Charts ◽

Basic Function ◽

Function Blocks ◽

Iec 61499

Download Full-text

Zero-Downtime Reconfiguration of Distributed Control Logic in Industrial Automation and Control

Reconfigurable Embedded Control Systems ◽

10.4018/978-1-60960-086-0.ch003 ◽

2011 ◽

pp. 55-81 ◽

Cited By ~ 2

Author(s):

Thomas Strasser ◽

Alois Zoitl ◽

Martijn Rooker

Keyword(s):

Control Systems ◽

New Technologies ◽

Reference Model ◽

Industrial Process ◽

Control Logic ◽

Control Applications ◽

Automation And Control ◽

Engineered Systems ◽

And Control ◽

Iec 61499

Future manufacturing is envisioned to be highly flexible and adaptable. New technologies for efficient engineering of reconfigurable systems and their adaptations are preconditions for this vision. Without such solutions, engineering adaptations of Industrial Process Measurement and Control Systems (IPMCS) will exceed the costs of engineered systems by far and the reuse of equipment will become inefficient. Especially the reconfiguration of control applications is not sufficiently solved by state-of-the-art technology. This chapter gives an overview of the use of reconfiguration applications for zero-downtime system reconfiguration of control applications on basis of the standard IEC 61499 which provides a reference model for distributed and reconfigurable control systems. A new approach for the reconfiguration of IEC 61499 based control application and the corresponding modeling is discussed. This new method significantly increases engineering efficiency and reuse in component-based IPMCS.

Download Full-text

IEC 61499 ontology model for semantic analysis and code generation

2011 9th IEEE International Conference on Industrial Informatics ◽

10.1109/indin.2011.6034946 ◽

2011 ◽

Author(s):

Wenbin Dai ◽

V. Dubinin ◽

V. Vyatkin

Keyword(s):

Code Generation ◽

Semantic Analysis ◽

Ontology Model ◽

Iec 61499

Download Full-text

Automated analysis of Stateflow models

10.29007/b8gq ◽

2018 ◽

Author(s):

Hamza Bourbouh ◽

Pierre-Loic Garoche ◽

Christophe Garion ◽

Arie Gurfinkel ◽

Temesghen Kahsai ◽

...

Keyword(s):

Code Generation ◽

Denotational Semantics ◽

Automated Analysis ◽

Cyberphysical Systems ◽

Modeling Framework ◽

Safety Verification ◽

Starting Point ◽

Compilation Process ◽

Modal Behavior ◽

Hierarchical State Machines

Stateflow is a widely used modeling framework for embedded and cyberphysical systems where control software interacts with physical processes. In this work, we present a framework and a fully automated safety verification technique for Stateflow models. Our approach is two-folded: (i) we faithfully compile Stateflow models into hierarchical state machines, and (ii) we use automated logic-based verification engine to decide the validity of safety properties. The starting point of our approach is a denotational semantics of Stateflow. We propose a compilation process using continuation-passing style (CPS) denotational semantics. Our compilation technique preserves the structural and modal behavior of the system. The overall approach is implemented as an open source toolbox that can be integrated into the existing Mathworks Simulink/Stateflow modeling framework. We present preliminary experimental evaluations that illustrate the effectiveness of our approach in code generation and safety verification of industrial scale Stateflow models.

Download Full-text

Type-Directed Partial Evaluation

DAIMI Report Series ◽

10.7146/dpb.v24i494.7022 ◽

1995 ◽

Vol 24 (494) ◽

Author(s):

Olivier Danvy

Keyword(s):

Programming Languages ◽

Code Generation ◽

Compiler Optimization ◽

Partial Evaluation ◽

Lambda Calculus ◽

Denotational Semantics ◽

Compiler Generation ◽

Environment Type ◽

Symbolic Evaluation ◽

Specialized Program

We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a ``dynamic initial environment´´. Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's ``inverse of the evaluation functional´´ (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.This paper therefore bridges partial evaluation and lambda-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and run-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.Proceedings of POPL96, the 1996 ACM Symposium on Principles of Programming Languages (to appear).

Download Full-text