MODEL-DRIVEN ENGINEERING OF COMPLEX SYSTEMS Supporting the Design of Reactive Systems with Augmented Modeling and Verification Mechanisms

Abstract

This thesis motivates the need for the Reactive Blocks approach for model-driven Complex Systems Engineering (CSE). With the booming of the Internet economy and development of the Internet of Things (IoT), interconnected applications have penetrated into areas including manufacturing, management, and all aspects of human life. Embedded devices and internet-based services are increasingly inter-connected, and as the applications and services grow, the devices are intertwined into a complex system. This approach comprises a core process that constitutes the practice of model-driven development, component-based distributed system synthesis and derivation, software verification, modeling and verification augmentation for a variety of properties, such as real-time, probabilistic properties of complex systems. We constrain CSE to distributed and concurrent reactive software systems that are prevalent in many application domains, such as avionics, consumer electronics, robotics and new emerging sensor networks. These domains need to address a variety of properties in software and hardware. The efforts involved in implementing a system correctly, consume the majority of the development time and cost of complex systems; thus, many design and verification methods have been devised and applied to software development to ensure correct implementation. The Reactive Blocks approach, initiated by the network systems group in the Department of Information Security and Communication Technology, Norwegian University of Science and Technology, is designed to use reusable building blocks to build systems with significantly reduced development time and cost while at the same time guaranteeing the functional accuracy and transparency. Reactive Blocks takes the UML activity and state machine diagrams as the main design unit and provides a visual programming interface, while the implementation details are hidden in the diagrams. Reactive Blocks allows more than specifying just functional properties, but also QoS properties like real-time and performance. To empower Reactive Blocks with QoS properties analysis in our approach, we imported and analyzed a graph representation of our approach. Based on the graph representation, we extended the verification of Reactive Blocks with augmented extensions and applied rich formal method based analysis. In the first part of the thesis, we analyze the graph representation in Reactive Blocks. To analyze the graph representation, we imported graph transformation rules for automatically analyzing the decomposition and automatic remedy of design errors in the system specification. This part involves two papers with one addressing the choreography model transformation via graph transformation rules and the other automatic system design error detection and remedy. Second, the modeling capabilities of Reactive Blocks are augmented and extended to include new formalisms. New system requirements are addressed using extended state transition diagrams. To describe the real-time constraints in building blocks, we extend and augment the external state machine (ESM) to a real-time ESM (RTESM) with clock variables and guard notations. Further, the augmentation capabilities consider possibilities and formalize the probabilistic RTESM (PRTESM). This part involves three papers addressing real-time modeling and verification, a performance index for building blocks, and probabilistic modeling and verification of reactive systems respectively. Third, with its extended modeling capabilities, the Reactive Blocks approach can be used in the modeling and verification of probabilistic real-time systems which are typical in cyber-physical systems, such as robots and aviation control systems. This is discussed in two papers. In one of them, we summarize a tool chain for the formal development of controllers for hybrid systems that need to fulfill both real-time and spatial behavior properties. In the other one, we depict a hybrid control system background and combine the simulation tool JEmula with our reactive system design and analysis. We also use the BeSpaceD tool for the 802.11 WLAN wireless signal strength and coverage area analysis, which facilitates the safe control of robots. Our CSE approach has a strong focus on formal methods. We use timed automata and probabilistic timed automata for interpreting the extended specification. In particular, we apply Timed Computation Tree Logic (TCTL) and Probabilistic Timed Computation Tree Logic (PTCTL) to verify timed probabilistic properties of the specification, and such formalisms (RTESM, PRTESM) inherit the compositional and incremental verification characteristics of our Reactive Blocks paradigm. We integrated several tools to support our approach, including AGG and HENSHIN for graph based model transformation, and we used the popular real-time verification tools UPPAAL and PRISM for time and probabilistic properties verification. These tools were integrated using self-developed software facilities that automatically migrate the syntax of different formalisms. The spatial properties simulation and verification were achieved by integrating Reactive Blocks with the spatial property verification tool BeSpaceD. We built the control function building blocks of robot controllers and simulation environments that generate output for the BeSpaceD tool. The embedded robot control system addresses the real-time and probabilistic properties of hybrid system. Traces of robot movements were analyzed, and certain spatial safety properties were verified by the BeSpaceD tool.