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.
Has parts
Paper A: Han, Fenglin; Kathayat, Surya Bahadur; Le, Hien Nam; Bræk, Rolv; Herrmann, Peter Michael. Towards Choreography Model Transformation via Graph Transformation. I: Proceedings 2011 2nd IEEE International Conference On Software Engineering and Service Science. IEEE Press 2011 ISBN 978-1-4244-9696-9. s. 508-515 https://doi.org/10.1109/ICSESS.2011.5982365 © 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.Paper B: Han, Fenglin; Herrmann, Peter Michael. Remedy of Mixed Initiative Conflicts in Model-based System Engineering. Electronic Communications of the EASST 2012 ;Volum 47. http://dx.doi.org/10.14279/tuj.eceasst.47.717
Paper C: Han, Fenglin; Herrmann, Peter Michael; Le, Hien Nam. Modeling and Verifying Real-time Properties of Reactive Systems. I: Engineering of Complex Computer Systems (ICECCS), 2013 18th International Conference on. IEEE conference proceedings 2013 ISBN 978-0-7695-5007-7. s. 14-23 https://doi.org/10.1109/ICECCS.2013.13 © 2013 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Paper D: Han, Fenglin; Herrmann, Peter Michael. Modeling Real-Time System Performance with Respect to Scheduling Analysis. 6th IEEE International Conference on Ubi-Media Computing (UMEDIA 2013); 2013-11-02 - 2013-11-04 https://doi.org/10.1109/ICAwST.2013.6765522 © 2013 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Paper E: Han, Fenglin; Blech, Jan Olaf; Herrmann, Peter Michael; Schmidt, Heinz. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. Electronic Proceedings in Theoretical Computer Science 2014 ;Volum 147. s. 1-15 http://dx.doi.org/10.4204/EPTCS.147.1
Paper F: Herrmann, Peter Michael; Blech, Jan Olaf; Han, Fenglin; Schmidt, Heinz. A model-based toolchain to verify spatial behavior of cyber-physical systems. International Journal of Web Services Research 2016 ;Volum 13.(1) s. 40-52 https://doi.org/10.4018/IJWSR.2016010103
Paper G: Han, Fenglin; Blech, Jan Olaf; Herrmann, Peter; Schmidt, Heinz. Model-Based Engineering and Analysis of Space-Aware Systems Communicating via IEEE 802.11. I: Computer Software and Applications Conference (COMPSAC), 2015 IEEE 39th Annual. IEEE 2015 ISBN 9781467365659. s. 638-646 https://doi.org/10.1109/COMPSAC.2015.46 © 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.