Software Abstractions and Human-Cyber-Physical Systems Architecture Modelling.

It is over fifty years since the subject discipline of software engineering and more than forty years from when the area of formal methods have been established. During this period, the academic community has accomplished extensive research in foundations and methods of software engineering, as well as developing and teaching a large body of software engineering knowledge and techniques. At the same time, the IT industry has produced larger, more complex, and better (in many aspects) software systems. Yet, these large projects are largely developed using a trial and error approach, without systematic use of the developed software engineering methods and tools. The cost of these projects is high, the percentage of project delay and cancellation is significant, and the dependability of the systems is low in many requirements. The most serious problem of this ad hoc development approach is that the development process is not repeatable and the systems developed are not well evolvable. This problem is particularly crucial for the design and implementation of modern networked distributed software systems, known as Human-Cyber-Physical Systems (HCPS). In this tutorial paper, we reflect the development of software engineering through software abstractions and show that these abstractions are integral in the notion of software system architectures. We discuss the importance of architecture modelling and argue for a seamless combination of informal and formal activities in the modelling and design of the architecture. A point that we make is that it is important to engineer systems using formal methods in relation to the definition and management of development processes, and how a model of the software architecture, with rich semantics and refinement relations, plays an important role in this process. We consider development of two typical types of software components and use examples to discuss the traditional processes for their domain modelling and software requirements modelling . We then propose to combine these modelling approaches and this naturally leads to a unified modelling process for HCPS architecture modelling, design, and evolution. Based on the unified processes, we outline a framework in engineering formal methods for HCPS modelling, including the mapping of the system architecture to the technology architecture and organization of the development team with the expertise required, and decide the appropriate formal methods and tools to be used.