Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Industrial automation devices have traditionally been programmed by engineers using standards such as IEC 61131–3 [17] and its derivatives. We see, however, novel trends according to which this well established procedure will change in the near future. One trend is the recent convergence of PC hardware and Programmable Logic Controllers (PLC) with respect to software development. In the past, industrial automation devices mostly relied on techniques and standards that were developed independently from PC hardware and IT technologies. Examples include the IEC 61131 standard for PLC and PROFIBUS [2] on the network technology side. In recent years, some PLC vendors started to integrate standard PC processors. Moreover, smart single-board computers like the Raspberry Pi [30] came into the market offering operating systems close to those of ordinary PCs. These boards are cheap but powerful enough to carry out control functions. For instance, we use Raspberry Pi-based devices to drive a bottling plant deployed in the RMIT’s advanced manufacturing precinct [13]. On the network technology side, the Ethernet has gained entry into the world of industrial automation.

Another trend is the growing interconnectivity of controllers. PLCs communicate now with each other and with other external devices and services, not just for synchronization and basic control via the Supervisory Control and Data Acquisition (SCADA) level, but also to support maintenance and new production processes making a higher degree of customization possible. The growing interconnectivity also allows for the utilization of novel technologies like cloud computing. For example, services analyzing data streams to determine maintenance intervals are already in place (see, e.g., ABB ServicePort [6]). Initiatives like Industry 4.0 [18] foster these trends as they propose interconnected plants run by controllers coordinating itself using internet-based services.

In our opinion, these trends in industrial automation will have growing relevance also with respect to the application of human-oriented formal methods. In particular, based on the more extended use of standard IT and PC technology, development paradigms from computer science can be applied in this area. This includes the use of model-based development as well as formal specification and verification technologies. Since many engineers have no in-depth experience with the application of the formal methods used in software development, we have to find a way lessening the burden of applying the formalisms in practice. One promising idea is Rushby’s concept of “Disappearing Formal Methods” [27] that proposes the wrapping of formal techniques into tools such that they are easy to use. Our model-based engineering technique Reactive Blocks [22] supports Rushby’s concept. In this article, we propose its use for the development of control software in industrial automation.

Fig. 1.
figure 1

The UML activity of building block ManageLEDoperation.

Full size image

2 Reactive Blocks in Industrial Automation

Reactive Blocks [3, 22] is a model-driven engineering technique for reactive Java-based systems. It uses UML activity and state machine diagrams [25] to model systems. Since these diagram types are innately not provided with formal semantics, we defined one ourselves. In [23], we defined an initial formal semantics for an early version of the tool based on cTLA [15], a variant of Lamport’s Temporal Logic of Actions (TLA) [24]. Becoming more experienced with the tool, we later defined the so-called reactive semantics [20]. Since UML activities are basically graphs, we based it on rules in traditional graph theory.

One of the features of Reactive Blocks is that sub-functionality can be specified separately from each other in so-called building blocks. That enables us to create models of recurring sub-functionality once and to reuse them in several engineering projects. The reuse is further facilitated by providing each building block with an External State Machine (ESM) [19]. This is a behavioral interface allowing us to combine a building block correctly with its environment without having to completely understand its functionality.

A UML activity is used to model the behavior of a building block. The activity depicted in Fig. 1 contains three inner building blocks of type Button, Toggle and LEDoperation that all embed certain sub-functionality. The reactive semantics of the activities resembles Petri nets and corresponds to the flow of tokens via the edges towards the nodes. In this way, control and data flows are nicely visualized and can also be animated by the tool-set. Further, activities may contain operations that represent Java methods executed when a token passes the corresponding node. The flows are run-to-completion (see [20]). That means, a flow passes all nodes on its way in the same atomic step until it reaches one that models the need to wait for a certain stimulus (i.e., a timeout or an external event).

To connect the flows of an activity containing an inner block and the one specifying the behavior of this block, we use so-called parameter nodes and pins. Parameter nodes are the little arrows at the outer edge of the activity. In the node representing an inner building block in an activity, the parameter nodes are shown as pins. For instance, the pins of the inner building block LEDoperation in Fig. 1 are identical to the parameter nodes in its activity (see Fig. 2). A flow reaching a pin of an inner building block will continue in the activity of this block from the corresponding parameter node and vice versa in the same run-to-completion step.

Thanks to the formal reactive semantics, we could build a model checker into the tool-set [22] enabling the verification that the UML models fulfill various correctness properties (e.g., the preservation of ESMs by the activities and deadlock freedom). Following the “Disappearing Formal Methods” concept [27] mentioned in the introduction, the formal issues of the verification process are hidden to the user of the tool, and traces towards erroneous states are animated directly on the UML activity graphs. The verification runs scale thanks to the separation of functionality into different building blocks. Moreover, the UML models can be automatically transformed into executable Java code [21].

In our opinion, the features of Reactive Blocks makes it highly suited for the development of control software in industrial automation. The building block concept fits well to the technical engineering disciplines, in which the same physical components are often used in different applications. So, when a particular pump or valve is reused in a certain chemical plant, the building blocks realizing the control of this component may be reused in the software model of the plant as well.

Also the fact that the UML activities visualize control and data flows, is helpful for the industrial automation domain since a typical property of control software is the large number of threads running in parallel. While the coordination of the threads is difficult in classical programming languages, the run-to-completion semantics together with the clearly arranged modelling of the control and data flows facilitates the coordination of the various threads significantly.

Applying the built-in model checker leads to less errors in the generated control software. Moreover, one can couple Reactive Blocks with other analysis tools. Of particular interest for industrial automation is the composition of the tool-set with BeSpaceD [5], a tool suited to verify spatiotemporal properties (see [14]). That allows us to check already on the modelling level that control software guarantees certain cyber-physical properties [16].

Another advantage of the building blocks and the ESMs is that the development of sub-functionality by various teams of experts can be nicely coordinated by embedding the sub-tasks in separate building blocks. Furthermore, the rich set of building block libraries supports the development of technical systems. For instance, the tool-set contains libraries containing various communication protocols as well as blocks supporting the design of Internet of Things applications [3] that play an important role in industrial automation. We show in Sect. 3 that building blocks for control and for communication can be easily combined (see also [12]). This fits nicely with the goals of Industry 4.0 [18].

3 Example

We demonstrate our approach by using a Raspberry Pi equipped with a Berry Clip, i.e., a board provided with six colored LEDs, a buzzer, and a switch. In our toy example, a lucent LED represents a certain production sub-process. To determine the strain of the “plant”, the number of changes between the LEDs shall be sent periodically to a remote control center.

Fig. 2.
figure 2

The UML activity of building block LEDoperation.

Full size image

We developed the control and communication software for the example by creating three building blocks in Reactive Blocks. Figure 2 depicts the UML activity describing the behavior of the building block LEDoperation that realizes the operation of the LEDs on the Berry Clip. The inner block of type LEDs contains the functionality to switch on and off the LEDs of the Berry Clip while TimerPeriodic realizes a recurring timer that sends flows in even intervals (three seconds in our example).

Fig. 3.
figure 3

The ESM of building block LEDoperation.

Full size image

The ESM of building block LEDoperation is shown in Fig. 3. The block is started by a flow through parameter node start which is forwarded to the pin of the same name at the inner block LEDs. Thereafter, the ESM is in state passive. In this state, a flow through the parameter nodes callCounter and counter is allowed. It can be used by the environment of the building block to retrieve the number of LED changes that are stored in the variable counter.

The rotative lighting of the LEDs is started by a flow through the parameter node on bringing the ESM into state active. As shown in the activity, the flow starts the periodic timer. A timeout leads to a flow through pin tick of block TimerPeriodic. This flow is forked into two flows. One flow retrieves the value of the LED currently switched on, that is stored in variable active, and forwards it to pin setOff of building block LEDs. Thus, the currently lucent LED is switched off. The other flow reaches a flow breaker. That is a special timer without a dedicated duration used to separate a flow into different run-to-completion steps. In our case, we use the flow breaker since the ESM of block LEDs does not accept flows through its pins setOff and setOn in the same run-to-completion step. The flow leaving the flow breaker reaches operation handleStep that represents a Java method determining the next LED to switch on, sets the selected value in variable active and increments the counter. After terminating the method, the flow forwards to pin setOn of building block LEDs such that the selected LED is switched on. A flow through parameter node off stops the lighting of the LEDs by terminating the periodic timer and switching all LEDs off. The building block can be terminated by a flow passing the parameter nodes stop and stopped.

Figure 1 shows the building block ManageLEDoperation modeling that the LEDs can be switched on and off by pushing the button of the Berry Clip. Here, LEDoperation is represented by an inner building block. Further, we use building block Button handling the access to the button of the Berry Clip and Toggle that allows us to lead button pushes mutually to the on and off pins of LEDoperation.

Fig. 4.
figure 4

The UML activity of building block SendStatus.

Full size image

The transmission of the number of LED changes is realized by building block SendStatus depicted in Fig. 4. We use the popular MQTT protocol, the functionality of which is handled by the inner block RobustMQTT. Further, SendStatus uses another periodic timer initiating a transmission every 30 s. A timeout leads to a retrieval of the current counter value by a flow through parameter node callCounter. The value is received via parameter node counter that is forwarded to operation makeMessage. The corresponding Java method creates an object containing the MQTT message format that is forwarded to the pin publish of block RobustMQTT triggering the transmission of the counter value. Moreover, the building block contains the inner block Buzzer that is used to give a short audio signal using the buzzer of the Berry Clip in order to show that the status value was sent.

The activity of the overall system model is quite simple. It consists of instances of building blocks ManageLEDoperation and SendStatus, initial triggers for these blocks, and edges connecting their pins callCounter resp. counter. We automatically transformed this system description into a runnable JAR file that can be directly executed on the Raspberry Pi. Moreover, we created another simple system model enabling us to receive and print out MQTT messages at a remote control station.

The toy example substantiates two of the advantages named in Sect. 2. One is reusability. The complex functionality, i.e., the activation of the various units of the Berry Clip as well as the transmission via MQTT had not to be programmed manually but could be reused by simply adding already existing building blocks. Thus, the only creative task was the link of the various building blocks. Therefore the models for the Berry Clip controller and the remote station could be created by one of the authors within less than an hour. The undertaking was supported by the model checker built into Reactive Blocks since we could easily find out if all the blocks were indeed correctly coupled preserving their ESMs.

The other advantage affirmed by the example is the coordination of development teams since one can hand the creation of the building blocks LEDoperation and ManageLEDoperation over to a team of control software experts and SendStatus to people with in-depth knowledge about communication. Also here the model checker is of great help since it guarantees that the teams realize the ESM-based behavioral interface descriptions of the particular blocks correctly such that the results of their work can be seamlessly coupled.

4 Related Work

Formal specification of Programmable Logic Controllers (PLC) is not new but most work is based on PLC specific programming and specification techniques (see, e.g., [26, 29]). Summaries of earlier approaches to use formal methods for the specification and verification of PLC programs is given in [1, 9].

One of the main disadvantages of the IEC standard 61131 [17] is that it leaves some implementation and semantics aspects open to the PLC vendors. This makes formal specification and verification work difficult, but it also hinders cross platform development efforts. Some approaches such as the UNICOS toolset [10] were developed to address these shortcomings. A comprehensive model checking approach for IEC 61131–3 programs in connection with UNICOS can be found in [8]. A transformation from UML into IEC 61131 has been studied in [31]. In [11], UML is used to model control software and analysis patterns together with cTLA (see [15]) to verify their correctness. We established Coq descriptions of IEC 61131–3 programs (see [4]) to facilitate human directed verification of PLC programs (see also [7]). Another formal approach based on IEC 61499 was proposed in [32]. Formal methods are also used to analyze Ethernet-based real-time communication [28].

5 Conclusion

In this paper, we motivated that systems bridging control automation with the classical IT world will become more mainstream in the close future. That opens the door for the application of model-based and formal methods in this application domain as well. In particular, we propose the use of Reactive Blocks for control applications in the industrial automation domain. We believe that, due to the easy use of the UML diagrams for modeling and the model checker for analysis, it facilitates the application of formal methods in the practical development of control system software also by users that are not experts in formal techniques. We exemplified our approach by discussing the development of a small Raspberry Pi-based system that, in spite of its size, is sufficient to point out some of the expected advantages.