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

Towards Topology-Free programming for Cyber-Physical Systems with process-oriented Paradigm

SENSORS 2023年第13期23卷 6216-6216页

作者： Zyubin, Vladimir E. Garanina, Natalia O. Anureev, Igor S. Staroletov, Sergey M. RAS Inst Automat & Electrometry SB Academician Koptyug Ave 1 Novosibirsk 630090 Russia

The paper proposes a topology-free specification of distributed control systems by means of a process-oriented programming paradigm. The proposed approach was characterized, on the one hand, by a topologically independent specification of the control algorithm and, on the other hand, by the possibility of using existing formal verification methods by preserving the semantics of a centralized process-oriented program. The paper discusses the advantages of a topologically independent specification of distributed control systems, outlines the features of control software, argues why the use of a process-oriented approach to the development of the automation of cyber-physical systems is suitable for solving these problems, describes a general scheme for implementing a distributed control system according to a process-oriented specification, and proposes a formal heuristic algorithm for partitioning a sequential process-oriented program into independent clusters. We illustrate our algorithm with bottle-filling and sluice case studies.

关键词： distributed control systems control software process-oriented programming topology-independent algorithm specifications hyperprocess

来源：评论

学校读者我要写书评

暂无评论

Safe design and evolution of smart contracts using dynamic condition response graphs to model generic role-based behaviors

引用

JOURNAL OF SOFTWARE-EVOLUTION AND process 2025年第1期37卷

作者： Xu, Yibin Slaats, Tijs Dudder, Boris Hildebrandt, Thomas Troels Van Cutsem, Tom Univ Copenhagen Dept Comp Sci Copenhagen Denmark Katholieke Univ Leuven Dept Comp Sci Distrinet Leuven Belgium

Smart contracts executed on blockchains are interactive programs where external actors generate events that trigger function invocations. Events can be emitted by participants asynchronously. However, some functionalities should be restricted to participants inhabiting specific roles in the system, which might be dynamically adjusted while the system evolves. We argue that current smart contract languages adopting imperative programming paradigms require additional complicated access control code. Furthermore, smart contracts are often developed and evolved independently and cannot share a joint access control policy. This makes it challenging to ensure the correctness of access control properties and to maintain correctness when the contracts are adapted. We propose using dynamic condition response (DCR) graphs for role-based and declarative access control for smart contracts and techniques for test-driven modelling and refinement of DCR graphs to support the safe design and evolution of smart contracts. We show that they allow for capturing and visualizing a form of dynamic access control where access rights evolve as the contract state progresses. Their use supports the straightforward declaration of access control rights, improved code auditing, test-driven modelling, and safe evolution of smart contracts and improves users' understanding. The paper introduces the use of dynamic condition response (DCR) Graphs for role-based and declarative access control in smart contracts. This approach enhances the security and adaptability of smart contracts by enabling dynamic role adjustments and visualizing access control rights. The methodology supports straightforward declaration of access control rights, improves code auditing, and facilitates the safe evolution of smart contracts. image

关键词： process-oriented programming refinement role-based programming safe evolution smart contract programming smart contract security test-driven modelling

来源：评论

学校读者我要写书评

暂无评论

Model Checking Programs in process-oriented IEC 61131-3 Structured Text

引用

AUTOMATIC CONTROL AND COMPUTER SCIENCES 2024年第7期58卷 1025-1041页

作者： Garanina, N. O. Staroletov, S. M. Zyubin, V. E. Anureev, I. S. Russian Acad Sci Inst Automat & Electrometry Siberian Branch Novosibirsk Russia

process-oriented programming is a paradigm based on the concept of a process. Each process is a finite-state machine (FSM). This paradigm is intended for programmable logic controller (PLC) developers to write software that supports Industry 4.0. The poST language is a promising process-oriented extension of the IEC61131-3 Structured Text (ST) language designed to provide conceptual consistency between the PLC source code and the process description of the controlled process. This language combines the advantages of FSM programming with the standard syntax of the ST language. We propose a transformational semantics of poST given by rules for translating poST language statements into Promela, the input language of the SPIN model checker. Following these rules, our Xtext-based translator builds a Promela model for the poST program. The main contribution of our article is the transformational semantics of poST and a method to automatically generate Promela code from poST control programs. The resulting Promela model is ready to be verified using the SPIN model checker against the requirements for the initial poST program expressed in terms of the linear temporal logic (LTL). In this article, we give an overview of related works as well as a brief description of the poST and Promela languages. The rules presented below for translating from poST to Promela cover control flow statements, constructs for creating processes and managing their states, as well as timeout statements. Service processes for modeling the external environment and specifying high-level LTL specifications are defined separately. Then we dwell on the main ideas of implementing the poST translator in Promela and further illustrate our approach using a system for managing the consumption and production of electricity, including renewable sources.

关键词： control software model checking process-oriented programming LTL SPIN Structured Text

来源：评论

学校读者我要写书评

暂无评论

Requirement Patterns in Deductive Verification of poST Programs

引用

AUTOMATIC CONTROL AND COMPUTER SCIENCES 2024年第7期58卷 1003-1024页

作者： Chernenko, I. M. Anureev, I. S. Garanina, N. O. Russian Acad Sci Inst Automat & Electrometry Siberian Branch Novosibirsk Russia

process-oriented programming is one of the approaches used to develop control software. A process-oriented program is defined as a sequence of processes. Each process is represented by a set of named states containing a program code that define the logic of the process' behavior. Program execution is a sequential execution of each of these processes in their current states at each iteration of the control loop. processes can interact through changing the states of each other and shared variables. This paper develops a method for classifying temporal requirements for process-oriented programs in order to simplify and automate the deductive verification of such programs. The method consists of the following steps. At the first step, the requirements are formalized in a specialized language DV-TRL, a variant of the typed first-order predicate logic with a set of interpreted types and predicate and functional symbols that reflects specific concepts of the control systems in the process-oriented paradigm. At the second step, the formalized requirements are divided into classes, each of which is defined by a pattern-a parametric formula of the DV-TRL language. The verification conditions generated for process-oriented programs with respect to the requirements satisfying the same pattern have the same proof scheme. At the third step, appropriate proof schemes are developed. In our paper, we first give a brief introduction to the poST language, a process-oriented extension to the ST language of the IEC 61131-3 standard. Next, the DV-TRL language is defined. We also provide a collection of natural language requirements for several control systems. Then we define the patterns that fully cover all the requirements of this collection. For each of these patterns, we give an example of a formalized requirement from the collection and describe a scheme for proving the verification conditions for this pattern. St-atistics on the distribution of requirements from the collection over

关键词： deductive verification temporal requirements requirement patterns control software process-oriented programming

来源：评论

学校读者我要写书评

暂无评论

poST: A process-oriented Extension of the IEC 61131-3 Structured Text Language

引用

IEEE ACCESS 2022年 10卷 35238-35250页

作者： Zyubin, Vladimir E. Rozov, Andrei S. Anureev, Igor S. Garanina, Natalia O. Vyatkin, Valeriy RAS SB Inst Automat & Electrometry Novosibirsk 630090 Russia Lulea Univ Technol Dept Comp Sci Elect & Space Engn S-97187 Lulea Sweden Aalto Univ Dept Elect Engn & Automat Espoo 02150 Finland

This paper presents the core concepts for the poST language - a process-oriented extension of the IEC 61131-3 Structured Text (ST) language which intends to provide a conceptual consistency of the PLC source code with technological description of the plant operating procedure. The poST can be seamlessly used as a textual programming language for complex PLC software in the context of IEC 61131-3 (3rd Edition). The language combines the advantages of FSM-based programming with the conventional syntax of the ST language which would facilitate its adoption. The poST language assumes that a poST-program is a set of weakly connected concurrent processes, structurally and functionally corresponding to the technological description of the plant. Each process is specified by a sequential set of states. The states are specified by a set of the ST constructs, extended by TIMEOUT operation, SET STATE operation, and START / STOP / check state operations to communicate with other processes. The paper describes the basic syntax of the poST language, demonstrates the usage of the poST language by developing control software for an elevator, and compares the development in poST with pure Structured Text.

关键词： Computer languages IEC 61131-3 standard PLC software development process-oriented programming

来源：评论

学校读者我要写书评

暂无评论

process-oriented programming Language for MCU-Based Automation

Process-Oriented Programming Language for MCU-Based Automati...

引用

International Siberian Conference on Control and Communications (SIBCON)

作者： Rozov, Andrei S. Zyubin, Vladimir E. Inst Automat & Electrometry SB RAS Novosibirsk Russia

ISBN: (纸本)9781479910625;9781479910601

process-oriented programming proves a powerful technique for building control and automation systems. The rising popularity of microcontroller-based automation makes it tempting to employ process oriented principles in such applications. However, existing process-oriented languages appear to be incompatible with major concepts of microcontroller programming. This paper discusses applicability of process-oriented programming principles to microcontroller-based systems development. An extended hyperprocess mathematical model is presented along with suggested syntax for a specialized programming language.

关键词： process-oriented programming microcontroller automation domain-specific language

来源：评论

学校读者我要写书评

暂无评论

Automatic Verification of Control Software in Cyber-Physical Systems with Plant Simulators

引用

OPTOELECTRONICS INSTRUMENTATION AND DATA processING 2019年第2期55卷 189-197页

作者： Lyakh, T. V. Zyubin, V. E. Garanina, N. O. Russian Acad Sci Inst Automat & Electrometry Pr Akad Koptyuga 1 Novosibirsk 630090 Russia Novosibirsk State Univ Ul Pirogova 2 Novosibirsk 630090 Russia Ershov Inst Informat Syst Pr Akad Lavrenteva 6 Novosibirsk 630090 Russia

The paper describes solving the problem of automatic verification of control software in cyber-physical systems created by means of process-oriented programming. A method based on plant simulators is proposed, and its... 详细信息

关键词： verification control software cyber-physical systems plant simulators process-oriented programming

来源：评论

学校读者我要写书评

暂无评论

Adaptation of the process-oriented Approach to the Development of Embedded Microcontroller Systems

引用

OPTOELECTRONICS INSTRUMENTATION AND DATA processING 2019年第2期55卷 198-204页

作者： Rozov, A. S. Zyubin, V. E. Russian Acad Sci Siberian Branch Inst Automat & Electrometry Pr Akad Koptyuga 1 Novosibirsk 630090 Russia Novosibirsk State Univ Ul Pirogova 1 Novosibirsk 630090 Russia

Adaptation of the process-oriented approach to programming of microcontrollers in embedded systems is described. Specific features of control software and programming of microcontrollers are analyzed. A mathematical model of the control software, which implies a mechanism of the description of microcontroller interruptions in the form of hyperprocesses, is proposed, and its dynamic semantics is provided. The model proposed in the study is a conceptual framework for the development of specialized languages of process-oriented programming of embedded systems.

关键词： embedded systems microcontrollers process-oriented programming hyperprocesses

来源：评论

学校读者我要写书评

暂无评论

Exploring Relationships between Syntax and Semantics of a process-oriented Language by Category Theory 8

Exploring Relationships between Syntax and Semantics of a Pr...

引用

8th International Conference on Ambient Systems, Networks and Technologies (ANT) / 7th International Conference on Sustainable Energy Information Technology (SEIT)

作者： Zhu, Ming Grogono, Peter Ormandjieva, Olga Shandong Univ Technol Coll Comp Sci & Technol Zibo Peoples R China Concordia Univ Dept Comp Sci & Software Engn Montreal PQ Canada

Recent research findings demonstrate that process-oriented programming languages provide a suitable means to develop concurrent systems. In this paper, we propose to use mandatory/optional trace sets to model the semantics of a process-oriented programming language named Erasmus. Inspired by Hoare's view of category theory and obtained research results towards validating the view, category theory is used to explore relationships between syntax and semantics of Erasmus. To illustrate the research activities, several examples are developed. In doing so, it is shown that a relationship between Erasmus commands can lead to a corresponding relationship between semantics for commands. 1877-0509 (C) 2017 The Authors. Published by Elsevier B.V.

关键词： Category theory Semantics Syntax process-oriented programming Erasmus

来源：评论

学校读者我要写书评

暂无评论

Exploring Relationships between Syntax and Semantics of a process-oriented Language by Category Theory

引用

Procedia Computer Science 2017年 109卷 241-248页

作者： Ming Zhu Peter Grogono Olga Ormandjieva College of Computer Science and Technology Shandong University of Technology Zibo China Department of Computer Science and Software Engineering Concordia University Montreal Canada

关键词： Category theory Semantics Syntax process-oriented programming Erasmus

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：