Quan Zu

Yilong Yang, Quan Zu, Peng Liu et al.

This paper takes up the problem of medical resource sharing through MicroService architecture without compromising patient privacy. To achieve this goal, we suggest refactoring the legacy EHR systems into autonomous MicroServices communicating by the unified techniques such as RESTFul web service. This lets us handle clinical data queries directly and far more efficiently for both internal and external queries. The novelty of the proposed approach lies in avoiding the data de-identification process often used as a means of preserving patient privacy. The implemented toolkit combines software engineering technologies such as Java EE, RESTful web services, JSON Web Tokens to allow exchanging medical data in an unidentifiable XML and JSON format as well as restricting users to the need-to-know principle. Our technique also inhibits retrospective processing of data such as attacks by an adversary on a medical dataset using advanced computational methods to reveal Protected Health Information (PHI). The approach is validated on an endoscopic reporting application based on openEHR and MST standards. From the usability perspective, the approach can be used to query datasets by clinical researchers, governmental or non-governmental organizations in monitoring health care and medical record services to improve quality of care and treatment.

Yilong Yang, Xiaoshan Li, Quan Zu

With the advancement of software engineering in recent years, the model checking techniques are widely applied in various areas to do the verification for the system model. However, it is difficult to apply the model checking to verify requirements due to lacking the details of the design. Unlike other model checking tools, LTSA provides the structure diagram, which can bridge the gap between the requirements and the design. In this paper, we demonstrate the abilities of LTSA shipped with the classic case study of the steam boiler system. The structure diagram of LTSA can specify the interactions between the controller and the steam boiler, which can be derived from UML requirements model such as system sequence diagram of the steam boiler system. The start-up design model of LTSA can be generated from the structure diagram. Furthermore, we provide a variation law of the steam rate to avoid the issue of state space explosion and show how explicitly and implicitly model the time that reflects the difference between system modeling and the physical world. Finally, the derived model is verified against the required properties. Our work demonstrates the potential power of integrating UML with model checking tools in requirement elicitation, system design, and verification.