scholarly journals Formal Verification of Cyberphysical Systems

Computer ◽  
2021 ◽  
Vol 54 (9) ◽  
pp. 15-24
Author(s):  
James Bret Michael ◽  
Doron Drusinsky ◽  
Duminda Wijesekera
Keyword(s):  
Formal Verification ◽  
Cyberphysical Systems

Formal Verification of Control System Software

2019 ◽  
Author(s):  
Pierre-Loïc Garoche
Keyword(s):  
Control System ◽  
Formal Verification ◽  
Formal Analysis ◽  
Critical Systems ◽  
System Software ◽  
Unified Approach ◽  
Verification Methods ◽  
Autonomous Cars ◽  
Computer Scientists ◽  
Verification Techniques

The verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. This book provides control engineers and computer scientists with an introduction to the formal techniques for analyzing and verifying this important class of software. Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. The book provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. It presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software. As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

HOL2GDT a Formal Verification-Based Design Methodology

2001 ◽  
Author(s):  
Anand Chavan ◽  
Byoung Woo Min ◽  
Shiu-Kai Chin
Keyword(s):  
Formal Verification ◽  
Design Methodology

Using computer clusters for processing spatial-temporal data streams in data acquisition systems

2018 ◽  
Vol 935 (5) ◽  
pp. 54-63
Author(s):  
A.A. Maiorov ◽  
A.V. Materuhin ◽  
I.N. Kondaurov
Keyword(s):  
Data Acquisition ◽  
Data Streams ◽  
Spatial Data ◽  
High Performance ◽  
Temporal Data ◽  
Cyberphysical Systems ◽  
Software Environment ◽  
Computer Clusters ◽  
Data Acquisition Systems ◽  
Essential Components

Geoinformation technologies are now becoming “end-to-end” technologies of the new digital economy. There is a need for solutions for efficient processing of spatial and spatio-temporal data that could be applied in various sectors of this new economy. Such solutions are necessary, for example, for cyberphysical systems. Essential components of cyberphysical systems are high-performance and easy-scalable data acquisition systems based on smart geosensor networks. This article discusses the problem of choosing a software environment for this kind of systems, provides a review and a comparative analysis of various open source software environments designed for large spatial data and spatial-temporal data streams processing in computer clusters. It is shown that the software framework STARK can be used to process spatial-temporal data streams in spatial-temporal data streams. An extension of the STARK class system based on the type system for spatial-temporal data streams developed by one of the authors of this article is proposed. The models and data representations obtained as a result of the proposed expansion can be used not only for processing spatial-temporal data streams in data acquisition systems based on smart geosensor networks, but also for processing spatial-temporal data streams in various purposes geoinformation systems that use processing data in computer clusters.

scholarly journals Data Driven Modelling of Nuclear Power Plant Performance Data as Finite State Machines

Modelling ◽  
2021 ◽  
Vol 2 (1) ◽  
pp. 43-62
Author(s):  
Kshirasagar Naik ◽  
Mahesh D. Pandey ◽  
Anannya Panda ◽  
Abdurhman Albasir ◽  
Kunal Taneja
Keyword(s):  
Power Plant ◽  
Nuclear Power Plant ◽  
Nuclear Power ◽  
Finite State Machine ◽  
State Machine ◽  
Plant Performance ◽  
Series Data ◽  
Cyberphysical Systems ◽  
Finite State ◽  
Machine Representation

Accurate modelling and simulation of a nuclear power plant are important factors in the strategic planning and maintenance of the plant. Several nonlinearities and multivariable couplings are associated with real-world plants. Therefore, it is quite challenging to model such cyberphysical systems using conventional mathematical equations. A visual analytics approach which addresses these limitations and models both short term as well as long term behaviour of the system is introduced. Principal Component Analysis (PCA) followed by Linear Discriminant Analysis (LDA) is used to extract features from the data, k-means clustering is applied to label the data instances. Finite state machine representation formulated from the clustered data is then used to model the behaviour of cyberphysical systems using system states and state transitions. In this paper, the indicated methodology is deployed over time-series data collected from a nuclear power plant for nine years. It is observed that this approach of combining the machine learning principles with the finite state machine capabilities facilitates feature exploration, visual analysis, pattern discovery, and effective modelling of nuclear power plant data. In addition, finite state machine representation supports identification of normal and abnormal operation of the plant, thereby suggesting that the given approach captures the anomalous behaviour of the plant.

Sign in / Sign up

Export Citation Format

Share Document