{'fraction_non_alphanumeric': 0.031084776663628078, 'fraction_numerical': 0.007019143117593437, 'mean_word_length': 5.078116343490304, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications

In this paper we address practical aspects of applying the model-checking method for industrial automation systems verification. Several measures are proposed to cope with the high computational complexity of model-checking. To improve scalability of the method, cloud-based verification tools infrastructure is used. Besides, closed-loop plant controller modelling and synchronization of transitions in the SMV (input language for symbolic model checking) model aim at complexity reduction. The state explosion problem is additionally dealt with by using an abstraction of the model of the plant with net-condition event systems, which is then translated to SMV. In addition, bounded model-checking is applied, which helps to achieve results in cases when the state space is too high. The paper concludes with comparison of performance for different complexity reduction methods.


Introduction
Formal verification is an act of proving or disproving an algorithm with respect to some specification or property and model-checking is one such formal verification approach introduced in early 1980s by Clarke and Emerson [1,2]. A model-checker generates state space of the model that includes all or some states and transitions. Each path in the state space corresponds to one system's run or a single test case. Model-checking enables the unsupervised automatic verification process of a system by generating the state space and identifies system failure via counterexamples (a scenario (state trace) that breaks the safety property of the system). Properties to be verified are specified using many methods, including temporal logic, automata, etc. While model-checking is computationally resource hungry, it has been successfully used in other adjacent areas of computer systems engineering, such as hardware design, proving its ability to handle problems of reasonably large complexity [3,4]. This suggests that it can be also applied in the industrial automation domain, and there have been impressive number of research works towards this goal [5,6]. For safetycritical applications, formal verification is one of the most efficient ways to prove system's correctness.

Cloud-based Model-Checking Infrastructure
Verification tasks consume many resources and verification process can run for days and block all important personal computer resources. In this section, we present how we could run verification remotely on a service such as Amazon Elastic Compute Cloud that grows according to the need. A verification problem usually contains specifications that are to be evaluated to prove or disprove many properties and each property checking can run as a separate process. Hence the option to perform verification tasks in the cloud instead of running them on an own computer provides performance related improvements. The cloud-based solution takes advantage of highly scalable parallel computations and more cost-efficiency in comparison to supporting own computation infrastructure. Fig. 1 shows possible decomposition of full verification with Bounded Model Checking (BMC). For each single bound, the NuSMV [7] verifier can generate a separate SAT-problem [7]. And all these SAT problems can be solved in parallel tasks (on many Amazon Cloud instances for example). In this work it is assumed that controllers are presented in terms of the function blocks of IEC 61499 standard that generalizes traditional programming paradigms of industrial automation for the case of component-based distributed systems.
For the function block models, memory consumption grows linearly for a single bound verification with NuSMV and this behaviour provides highly predictable resource needs. Reconfigurable clouds such as example Amazon EC2, enables us to tune cloud resources for specific model and reach high cost-efficiency.

Model Reduction with Plant Abstraction
In model-checking one of the most common problems is the state space explosion [8], which is tackled by various techniques [9]. In this section we present an abstraction technique in order to reduce the state space of the formal model that we use. This abstraction is built on top the closed-loop modelling previously proposed in modelchecking of function block systems [10].

Plant Model Abstraction using Net Condition-Event Systems (NCES)
In the closed-loop framework, both controller and plant are modelled with formalism, and then the combined model is exposed to model-checking. The controller model is automatically generated from the function block source code, using the function block (FB) operational semantics [11]. Therefore abstractions cannot be applied to the controller's model without loss of important execution aspects, hence we abstract on the model of the plant.
The control signals actuating the plant can be both value (level) and event (edge) signals. The formalism of NCES [12,13] has sufficient expressiveness to represent them.
In works [10,14] modelling and verification of closed-loop automation systems using NCES was described. In work [15] the methods to model Petri net in SMV [16] were proposed. Using first and second methods in combination with event signal transfer rules from FB operational semantics, hierarchical NCES models can be transformed into SMV.
The NCES model is wrapped into FB SMV module interface and contains input transition-place pairs ( Fig. 2 (a)) which are designed such that all input transitions are fired synchronously. If an activation event occurs, transition rewrites place marking regard to 'data input' value, for simple plant models with Boolean inputs, considered in this paper, the place becomes marked if 'data input' value is TRUE, otherwise the place becomes unmarked.  [15] can be transformed into NCES transition with event trigger by adding an event in 'enable' rule and simple unconditional event reset statement.
This approach mainly corresponds to events in FB operational semantics. The code snippet below shows the SMV module with the changes, line 2 shows the enable rule and the 'next()' statements show setting/resetting rules.  Fig. 3 (a) shows the 3-cylinder Pick-and-Place manipulator case study. It consists of 2 vertical and 1 horizontal cylinders and a suction unit (vacuum). Each cylinder has two sensors indicating two end positions of the piston. Full model verification with NCES was described in works [10,14], in this paper we propose a way to verify full operational semantics-based controller model [11] with plant abstraction.  [17] and the NCES plant model. At the initial state, the input 'INIT' has value 'TRUE', which corresponds to the occurrence of event 'INIT' in the beginning of execution. Event output 'INITO' is connected to input 'REQ'. This connection provides an entry point for system's main execution path, which may be described as a cycle of the occurrence of events REQ -> CNF -> CYL_IND -> CHG -> REQ ->… Also, input pp1 is 'true' and pp2 and pp3 are 'false' (workpiece is present in place 1 and places 2 and 3 are empty) for model testing. But in real systems checking these variables can be left "free" to verify all possible system states, or they can be connected to environment emulation module.

Example: A 3 Cylinder Pick-n-Place Manipulator
The simplest abstract model of the cylinder consists of only two states: 'home' and 'end' and two transition between these states. Transition emits event 'CHG' when it fires. Vacuum model contains only two states as well. Fig. 4(a) shows simple NCES models for vacuum and cylinder modules. The vacuum module has two inputs 'vacuum_on' and 'vacuum_off' and two outputs: 'vacState' and event 'CHG'. Two places 'On' and 'Off' represent simple vacuum states and transitions between this states emit event 'CHG' when fire. Cylinder model has two inputs and two states as well, but transitions with inhibitor arcs provide operation regard to rules: = & ; Fig. 4(b) shows the plant model with synchronous transitions inside the FB interface (wrapper). Inputs of NCES cylinders and vacuum are connected to synchronous transition-place pairs and outputs are merged with wrapper's outputs (in this case, event signal buffers reset is managed by wrapper and "outer" SMV module regard to FB operational semantics).

SMV Processes
Most of SMV language implementations support asynchronous module instances, implemented with keyword 'process' [16]. Usage of asynchronous processes provides simple representation or concurrent tasks but analysis of all possible execution orders together with increasing number of processes causes exponential state space growth (so-called state space combinatorial explosion). This problem affects resource consumption, for example memory and verification time. FB application SMV model, based on FB operational semantics, proposed in work [11] uses FB instance mapping to asynchronous SMV processes. This approach provides intuitively clear FB types and instances mapping and allows avoiding the problem with access of multiple modules to one signal buffer. It is also the simplest way to model asynchronous execution discipline in SMV. Fig. 5 shows access of two modules to event signal buffer. Value 'TRUE' of the buffer SMV variable means the event occurred and has not been read yet. So one module "puts" an event to the buffer (set TRUE value to the buffer SMV variable) and another module receives event (reads the variable) and resets SMV variable value to FALSE.

Synchronous Module Instances with External Buffer Controller
The approach to solve the multiple access problems with synchronous modules is based on external buffer controller, which contains all assignments of the shared buffer.

Synchronous FB Modules with Buffer Controller in SMV
In the function block SMV model, the execution order is fully determined by dispatchers. The problem of concurrent access to SMV variable occurs in event signal buffers, which are accessible from composite FB and its components. In this case, the schema shown in (b) Fig. 6(a) can be modified and external buffer controller can be placed in a composite FB as it is shown in (b) Fig. 6 Table 1 shows comparison of RAM usage and verification time for full PnP model and reduced with the first approach (described in section 3). Table 2 shows comparison of RAM usage and verification time for bounded model checking with single bounds for PnP model with asynchronous modules and synchronous ones.

Conclusion
Proposed modification of function blocks SMV models with synchronous modules allows for reduction of BMC verification time to reasonable limits. And the abstraction technique, using NCES to represent plant model, allows us to reduce model complexity when it necessary to keep within memory limits. Both, these techniques allow us to apply model-checking for verification of IEC 61499 closedloop systems, and make this approach cost-efficient with cloud technologies.