by Frank Alexander Kraemer and Peter Herrmann
Reactive Blocks is a toolkit to create, analyse and implement reactive applications. It helps developers to get concurrency issues right, reuse existing solutions, and brings model checking to the common programmer.
Internet of Things (IoT) applications connect hardware to communicate within a network, often with constrained resources. Therefore, even simple use cases quickly become very complex. In addition, IoT applications often combine several technologies, and only few programmers have the skill set to cover them all.
Model-driven development and model checking provide solutions to these problems. However, these solutions are barely used by programmers. Reasons for this are that model checking requires deep knowledge in formal methods to produce an appropriate input model that can be analysed. In addition, model-driven approaches often fail to cover details in code in a suitable way.
With these concerns in mind, we developed the Reactive Blocks tool for event-driven and concurrent applications. It has its origins at the Department of Telematics at the Norwegian University of Science and Technology (NTNU), and has been further developed by the spin-off company Bitreactive.
Building IoT Applications with Reactive Blocks
To appeal to the common programmer, the tool combines programming and modelling with an automatic compositional analysis, as shown in Figure 1: A developer creates a system from building blocks. Many of the blocks do not need to be developed from scratch but can be selected from libraries (1) The blocks are connected with each other (2) This is facilitated by behavioural contracts enabling the developer to understand the interface behaviour of a block without having to understand its inner details. Applications consist of a hierarchy of blocks. The applications are then analysed by automatic model checking. Once consistent, code is automatically generated and can be deployed as OSGi bundles or standalone Java applications (3).
Figure 1: The Reactive Blocks workflow. Blocks from libraries are combined to applications. Blocks are model-checked, and the application built via code generation.
To balance the benefits of generating code with that of manual programming, Reactive Blocks uses a combination of Unified Modelling Language (UML) with Java. UML describes the concurrent behaviour of building blocks with activity diagrams or state machines. State machines are also used to describe the contract of a block. The UML models only coordinate concurrent behaviour, and refer to Java methods for detailed operations on application programming interfaces (APIs) or other data. The Java methods are edited in the Java tools within Eclipse. Existing code can also be integrated, by encapsulating it into operations and building blocks. The code related to concurrency, i.e., code that decides when the operations are called, is generated from UML. This is usually the kind of code that is cumbersome and error-prone to write manually.
Compositional Analysis
A model checker is built into the editor. The building blocks have a formal semantics and correspond to temporal logic formulas, so that the model checker can take the UML model as input. Developers can start model checking with a single click. The encapsulation of building blocks by contracts enables a compositional analysis, in which each block can be analysed separately. This minimises the problem of state space explosion. An error is shown to the developer as animation in the editor such that can be easily understood and fixed. Examples of errors are deadlocks or violations of protocols, which are detected because the UML model of the building blocks do not reach their final state, or because the external contract of a block is violated. In addition, the tool detects if an application does not honour the life cycle contract of a component when it runs in a framework like OSGi. Such errors are hard, if not impossible, to detect by testing. The mathematical basis of the building blocks in temporal logic formulas makes it possible to reason about other properties, such as reliability, security [1], real-time properties [2], or spatial constraints [3].
Fleet Monitoring Case Study
A case study was developed within the IMSIS project funded by the Norwegian Research Council. It consists of a system that monitors a fleet of trucks while they deliver goods. Their position relative to defined geo-fences is constantly monitored and compared to expected arrival times. The backend system is informed about the arrival of freight. In case of deviations, alerts via email and SMS are sent. The system was created by programmers without specific knowledge in formal methods. Due to the built-in analysis, all interactions work correctly. Using building blocks, about 60% of the functionality could be taken from reusable libraries.
Link:
http://bitreactive.com
References:
[1] L.A. Gunawan, P. Herrmann: ”Compositional Verification of Application-Level Security Properties, in proc. of ESSoS 2013, LNCS 7781, February/March 2013.
[2] Han F., P. Herrmann: ”Modeling Real-Time System Performance with Respect to Scheduling Analysis”, in proc. of UMEDIA 2013, Aizu-Wakamatsu, IEEE Computer Society Press, September 2013.
[3] P. Herrmann, J.O. Blech, F. Han, H. Schmidt. A Model-based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems. In 2014 Asia-Pacific Services Computing Conference (APSCC), IEEE Computer.
Please contact:
Frank Alexander Kraemer, Peter Herrmann
NTNU, Norway,
E-mail:
