High-confidence Embedded Software Development Based on UML2.0 Communication Diagram and Temporal Logic

摘要

UML has actually become the industry standard in the field of embedded software modeling at present. However, the lack of precise semantics makes it difficult to analyze and validate models it describes. The executable linear temporal logic language XYZ/E can represent both static semantics and dynamic semantics. Based on these, a practical scheme combining UML2.0 communication diagram and XYZ/E to develop highconfidence embedded software is proposed. The UML2.0 communication diagram model of software is first defined its XYZ/E temporal logic semantics. Then based on the XYZ/E's characteristics of supporting stepwise refinement and model checking, we obtain reliable model of the system. Finally, the model is translated into C or Java codes automatically with the aid of the XYZ/E tools.