| 1. |
- Pakonen, Antti, et al.
(författare)
-
Evaluation of visual property specification languages based on practical model-checking experience
- 2024
-
Ingår i: Journal of Systems and Software. - : Elsevier. - 0164-1212 .- 1873-1228. ; 216
-
Tidskriftsartikel (refereegranskat)abstract
- Formal verification methods like model checking can provide mathematical proofs of design correctness, so their use is justified in applications where safety or reliability requirements are high. A key challenge for the wider adoption of model checking is the effort and expertise needed in formalizing functional requirements into verifiable properties. A particular challenge in specifying formal properties for industrial instrumentation and control (I&C) logics is accounting for the sequencing and timing issues that arise from, e.g., the dynamic behavior of the plant being controlled. In this paper, we evaluate different visual property specification languages that are aimed at making formal methods more accessible. We have collected 3923 formal properties from practical model checking projects in the nuclear and rail traffic industries and identified the most commonly occurring types of properties. Based on the sample data, a real-world example logic, and our practical experience, we identify requirements for a user-friendly property specification language most suited for our specific domain of industrial I&C.
|
|
| 2. |
- Zhang, Xiaojing, et al.
(författare)
-
Cooling Energy Consumption Investigation of Data Center IT Room with Vertical Placed Server
- 2017
-
Ingår i: Energy Procedia. - : Elsevier. - 1876-6102. ; 105, s. 2047-2052
-
Tidskriftsartikel (refereegranskat)abstract
- As energy consumption by cooling data center IT equipment can be over 40 % of total energy consumption, efficient cooling for large data centers is essential for reducing operation costs. Modern data centers are complex systems involving IT facilities, power system, cooling and ventilation systems. In our previous work, literature study was made to investigate available data center energy consumption models; and energy consumption models for data center IT room with distributed air flow control were developed. In this paper, the models are further extended and developed to cover the combined distributed air flow control and vertical placed servers in raised floor ventilation system. Simulation of the three types of ventilation systems with Even load, Idle server and Uneven load scenarios showed that significant cooling energy consumed by a traditional ventilation system can be saved by applying the proposed new concept and method. (C) 2017 The Authors. Published by Elsevier Ltd.
|
|
| 3. |
- Lilli, Giordano, et al.
(författare)
-
Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499
- 2023
-
Ingår i: IEEE Open Journal of the Industrial Electronics Society. - : Institute of Electrical and Electronics Engineers Inc.. - 2644-1284. ; 4, s. 417-431
-
Tidskriftsartikel (refereegranskat)abstract
- Automation systems within nuclear laboratories are intended to work under harsh operating conditions. Selective Production of Exotic Species (SPES) is a nuclear research facility currently under construction by the Istituto Nazionale di Fisica Nucleare, dedicated to the production and study of radioactive ion beams. Isotopes are produced within the target ion source unit, a vacuum vessel that must be replaced on a regular basis. The highly radioactive environment necessitates the deployment of a set of automated systems dedicated to the unit's remote management. To meet high-level security standards, the design of such instrumentation and control systems must include extensive verification. Based on specific safety requirements, model checking can be used to assess the systems' correctness. This article describes how to employ an integrated toolchain to design, simulate, formally verify, and deploy the control software for the Horizontal Handling Machine, a safety-critical remote handling system in operation at SPES. The IEC 61499 standard's adoption led to a redesign of the control logic. Following a preliminary online simulation, the closed-loop system has been formally verified using the NuSMV symbolic model checker, with the help of the FB2SMV converter. In addition, the Function Blocks Modeling Environment tool was used for automating verification and analyzing counterexamples.
|
|
| 4. |
- Yang, Chen-Wei, 1987-
(författare)
-
Cyber-Physical Engineering of Distributed Automation Systems in Energy Domain
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The main focus of this thesis is in the domain of Energy Systems, specifically in the engi-neering of modern Smart Grid (SG) automation systems. The SG has been categorizedas a Cyber-Physical System (CPS), a complex system which exhibits tight integration between the cyber and the physical processes and their interactions in a networked envi-ronment. The complexity and the computation of the automation system are expectedto increase with the promise of a ”smart” electric grid which is capable of self-healing, self-reconfiguration and become more resilient against cyber-attacks. These automation software systems require control strategies which are distributed in execution and requirevery tight integrations and interactions between various modular software and hardware components. As the automation system becomes more software intensive, we hypothesizethat existing design practices of developing the substation automation software system would struggle to cope with the distributed design challenges of the Smart Grid and they could be substantially enhanced by the application of model-driven design, distributed software architectures and semantic models.Model-driven engineering (MDE) is a software design paradigm that leverages the use of abstraction models at different stages of the design process for engineering complex software systems. MDE is widely used in the software engineering domain and it has proven to be effective when designing and maintaining large-scale software applications.One of the core tenants of MDE is model transformation and it is considered the heartand soul of MDE. The standard modelling language that is used for MDE in software engineering is the Unified Modelling Language (UML), which is a visual language with awide array of tool support. Despite its popularity in the software domain, UML models still have its limitations. In particular, the lack of uniformed semantics between its 13different visual diagrams and the lack of formal notations. In this thesis, we proposethe Cyber-Physical Engineering (CPE) framework, an MDE framework which combines semantic models and MDE based automatic model transformation in order to auto-generate both the automation control system and the simulation plant model from thephysical and functional specifications of CPS systems.All the scientific papers included in this thesis contributes towards the proposed Cyber-Physical Engineering methodology which includes MDE using semantic models, formal modelling of functional requirements and co-simulation testing of CPS systems.The contribution of the thesis is fivefold. Firstly, the thesis proposes the CPE frame-work, which is based on the use of semantic web modelling language where logical rea-soning can be applied to the models. The modelling language that is used is the Web Ontology Language (OWL), which is a declarative language with a strong formal foun-dation based on description logic. Secondly, the extended Semantic Web Rule Language(eSWRL) is introduced which defines the constructors that are necessary for model trans-forming OWL ontology models. The eSWRL transformation language is proposed to bean extension to the widely used ontology reasoning language Semantic Web Rule Lan-guage (SWRL) in order to address the limitations of monotonicity which restricts SWRLfrom transforming ontological models. Thirdly, the implementation of the underlying transformation engine of eSWRL in SWI Prolog. Fourthly, the formal modelling of func-tional requirements in ontology is proposed which investigates the viability of using nat-ural language based functional requirements to add control flow to the auto-generated automation control system. Lastly, an automated script based co-simulation environ-ment is shown to demonstrate how black-box validation can be performed to test theauto-generated automation control system.Finally, the thesis presents the resultant CPE framework for the modelling and genera-tion of distributed CPS automation software that leverages the use of semantic web OWL models. It is aimed to provide a top-down design approach of developing distributed con-trol software for CPS systems along with the simulation model of the physical plant. Inthis thesis, we demonstrate the development process of the CPE framework and throughcase study applications, how a semi-complete distributed automation software system in IEC 61499 can be automatically generated from substation specifications in IEC 61850 and natural language based functional requirements which provide the structure and thecontrol flow of the distributed automation software respectively. An eSWRL toolchainhas been developed to facilitate the various model transformation process of the CPE framework.
|
|
| 5. |
- Wang, Jia, et al.
(författare)
-
Industry-friendly engineering tools for wireless home automation devices
- 2015
-
Ingår i: Proceeding - 2015 IEEE International Conference on Industrial Informatics, INDIN 2015. - Piscataway, NJ : IEEE conference proceedings. - 9781479966493 ; , s. 1174-1179
-
Konferensbidrag (refereegranskat)abstract
- Although home automation (HA) systems in the wired domain are widely accepted by consumers, in today's industry, the mega trend is steering HA systems along a wireless way. Theoretically, wireless solutions are able to provide HA systems with more flexibility and thus reducing engineering costs. In practice, however, deploying wireless HA systems actually requires more costs and efforts due to the lack of versatile software tools to support the whole engineering process. This paper defines and evaluates the engineering workflow and architecture for home automation systems. The proposed architecture is studied and implemented based on web technologies and graphical configuration environments, with the aim of reducing workloads of HA engineers at every stage. A prototype has been implemented to demonstrate the technical feasibility of the proposed architecture.
|
|
| 6. |
- Kleyko, Denis, 1990-, et al.
(författare)
-
Distributed Representation of n-gram Statistics for Boosting Self-organizing Maps with Hyperdimensional Computing
- 2019
-
Ingår i: Perspectives of System Informatics. - Cham : Springer. ; , s. 64-79, s. 64-79
-
Konferensbidrag (refereegranskat)abstract
- This paper presents an approach for substantial reduction of the training and operating phases of Self-Organizing Maps in tasks of 2-D projection of multi-dimensional symbolic data for natural language processing such as language classification, topic extraction, and ontology development. The conventional approach for this type of problem is to use n-gram statistics as a fixed size representation for input of Self-Organizing Maps. The performance bottleneck with n-gram statistics is that the size of representation and as a result the computation time of Self-Organizing Maps grows exponentially with the size of n-grams. The presented approach is based on distributed representations of structured data using principles of hyperdimensional computing. The experiments performed on the European languages recognition task demonstrate that Self-Organizing Maps trained with distributed representations require less computations than the conventional n-gram statistics while well preserving the overall performance of Self-Organizing Maps.
|
|
| 7. |
- Lyu, Tuojian, et al.
(författare)
-
Mechatronic Swarm and its Virtual Commissioning
- 2023
-
Ingår i: Proceedings - 2023 IEEE International Conference on Mechatronics. - : Institute of Electrical and Electronics Engineers Inc.. - 9781665466615 - 9781665466622
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a swarm-based architecture for the composition of mechatronic systems from smart components complemented by a Virtual Commissioning (VC) environment. The architecture is based on the IEC 61499 standard. The proposed solution enables plug-and-play composition of the system which is ready to operate ”out of the box” right after it was composed without extra programming.
|
|
| 8. |
- Drozdov, Dmitrii
(författare)
-
Development and Verification of Dependable Software of Cyber-Physical Systems using Time-aware Computations
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Wired and wireless networking is becoming a necessary part of industrial control systems’ design and is one of the reasons that required a new cyber-physical approach to modelling. The phenomenon observed in cyber-physical systems (CPS) is a variety of cross-dependencies and influences between physical processes, computational devices and communications, which needs to be taken into account at the design and verification stage. Since most of the systems' functionality nowadays is implemented via software, the ability of software to be agnostic to the mentioned cross-influences is of high importance. This work introduces a concept called time-aware computations (TAC), which, instead of aiming at determinism, that is very expensive in distributed systems, aims at adaptability and robustness. It is based on the event-timestamping mechanism and is intended to let the developer handle each communication delay case individually thus minimizing its impact on functional properties of the automation system. It allows the controller to take into account actual point-to-point delay of the measured sensor readings, and adjust the control reaction accordingly, instead of trying to put the upper bound on it and wait for the maximum possible delay time. In industrial automation, the function block architecture of the IEC 61499 standard is increasingly used for modelling complex distributed automation systems. It is based on the concepts of event-driven block diagrams, and originally was created as a new programming paradigm for industrial automation controllers, but as a number of recent studies show, it also allows (and has been used) for modelling of CPS composed of physical processes combined with control and communication.The second major co-contribution of this work is a formal model of IEC 61499-based systems with timestamps that allows for modelling and verification of control logic (and closed-loop models) designed with TAC approach in mind. This would also allow for application of model-driven design methodologies later down the road.Third contribution is a software tool-chain that aims to greatly reduce the engineering work when applying formal verification to the designed systems.The proposed contributions' feasibility and effectiveness are demonstrated on a number of case studies.
|
|
| 9. |
- Faqrizal, Irman, et al.
(författare)
-
Probabilistic Model Checking for IEC 61499: A Manufacturing Application
- 2024
-
Ingår i: 25th International Conference on Industrial Technology (ICIT 2024). - : IEEE.
-
Konferensbidrag (refereegranskat)abstract
- The ever-increasing complexity of industrial control systems generates a demand for reliable development methods. IEC 61499, a recent industrial standard, helps to develop complex distributed systems based on their positive characteristics, namely reusability, reconfigurability, interoperability, and portability. Formal verification techniques, such as model checking, have been proposed to ensure the correctness of these systems during the design time. However, they do not consider the presence of the environment that can impact the application behaviour at runtime. This work combines design time and runtime analyses to apply probabilistic model checking on an IEC-61499-based manufacturing application. We present several probabilistic properties to be checked. The results are visualised graphically to be analysed, which allows one to optimise the system's quantitative features, such as productivity.
|
|
| 10. |
- Kleyko, Denis, 1990-, et al.
(författare)
-
Hyperdimensional computing in industrial systems : the use-case of distributed fault isolation in a power plant
- 2018
-
Ingår i: IEEE Access. - : IEEE. - 2169-3536. ; 6, s. 30766-30777
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an approach for distributed fault isolation in a generic system of systems. The proposed approach is based on the principles of hyperdimensional computing. In particular, the recently proposed method called Holographic Graph Neuron is used. We present a distributed version of Holographic Graph Neuron and evaluate its performance on the problem of fault isolation in a complex power plant model. Compared to conventional machine learning methods applied in the context of the same scenario the proposed approach shows comparable performance while being distributed and requiring simple binary operations, which allow for a fast and efficient implementation in hardware.
|
|
