EHSTM: a formal model of embedded software and research on several key issues

The traditional system design method cannot guarantee the dependence of large-scale and complex real-time embedded software. The model constructed by UML and other semi-structured modeling languages does not support simulation and verification, nor can it find requirements omission and logic contradiction. The Extended Hierarchical State transition Matrix model ( EHSTM ) which supports hierarchical modeling and concurrent States is proposed. The formal modeling of large-scale software system is simplified by model hierarchy. All relations between any two complex system concepts are clarified by hierarchical States and state parallelization, and the parallel behavior modeling of system is supported at the same time. After the model is constructed, it can be simulated and verified by a bounded model verification tool "GarakabuII". C source codes can be generated automatically after model checking and verification. In this way, system developers can focus only model design, which simplifies the system design process. Finally, a system design tool ZIPC based on EHSTM model is designed. Aiming at the problems of atomicity violation and data race in concurrent program development, ZIPC tool is used to construct the model, and the above problems can be effectively solved by experimental verification.