Publications

We present a new formal validation method for healthcare security policies in the form of feedback-based queries to ensure an answer to the question of Who is accessing What in Electronic Health Records. To this end, we consider Role Based Access Control (RBAC) that offers the flexibility to specify users, roles, permissions, actions, and the objects to secure. We use the Z Notation for formal specification of RBAC security policies and for queries to review these security policies. To ease the effort in creating the correct specification of the security policies, RBAC-based graphical models (such as SecureUML) are used and automatically translated into the corresponding Z specification. Both the specification of the queries and the specification of the policies are then animated using the Jaza tool to execute queries against the specification. By this it is automatically shown who will access the medical record of a patient and what information will be exposed to a system user.

In order to precisely analyze healthcare workflows, we examine how healthcare workflows can be modeled and verified with an elementary and concise timed CSP extension. To avoid considering healthcare workflows in isolation, we investigate the usage of our CSP dialect for formally modeling workflows alongside the instruction model of the openEHR specification set, which is a general, maintainable, and interoperable approach to electronic health records. Hence, we present a CSP model for openEHR instructions, which allows timed reasoning, and also integrates a basic notion of data and undefinedness. We show that this CSP dialect is suited to verify important properties of healthcare workflows, like workflow consistency, checking against timed specifications, and resource scheduling.

Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Integration aims at supporting collaborative healthcare workflows (CHWF) for improvement in sharing healthcare information and resources, efficiency of services and patients safety. CHWF are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modelling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We also follow the idea of UML of some visualized models, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work.

Objective
We present a dental training simulator that provides a virtual reality (VR) environment with haptic feedback for dental students to practice dental surgical skills in the context of a crown preparation procedure. The simulator addresses challenges in traditional training such as the subjective nature of surgical skill assessment and the limited availability of expert supervision.Methods and materials
We identified important features for characterizing the quality of a procedure based on interviews with experienced dentists. The features are patterns combining tool position, tool orientation, and applied force. The simulator monitors these features during the procedure, objectively assesses the quality of the performed procedure using hidden Markov models (HMMs), and provides objective feedback on the user's performance in each stage of the procedure. We recruited five dental students and five experienced dentists to evaluate the accuracy of our skill assessment method and the quality of the system's generated feedback.

Results
The experimental results show that HMMs with selected features can correctly classify all test sequences into novice and expert categories. The evaluation also indicates a high acceptance rate from experts for the system's generated feedback.

Conclusion
In this work, we introduce our VR dental training simulator and describe a mechanism for providing objective skill assessment and feedback. The HMM is demonstrated as an effective tool for classifying a particular operator as novice-level or expert-level. The simulator can generate tutoring feedback with quality comparable to the feedback provided by human tutors.

 We have developed a haptic virtual reality system for dental skill training. In this study we examined several kinds of kinematic information about the movement provided by the system supplement knowledge of results (KR) in dental skill acquisition. The kinematic variables examined involved force utilization (F) and mirror view (M). This created three experimental conditions that received augmented kinematic feedback (F, M, FM) and one control condition that did not (KR-only). Thirty-two dental students were randomly assigned to four groups. Their task was to perform access opening on the upper first molar with the haptic virtual reality system. An acquisition session consisted of two days of ten trials of practice in which augmented kinematic feedback was provided for the appropriate experimental conditions after each trial. One week after, a retention test consisting of two trials without augmented feedback was completed. The results showed that the augmented kinematic feedback groups had larger mean performance scores than the KR-only group in Day 1 of the acquisition and retention sessions (ANOVA, p<0.05). The apparent differences among feedback groups were not significant in Day 2 of the acquisition session (ANOVA, p>0.05). The trends in acquisition and retention sessions suggest that the augmented kinematic feedback can enhance the performance earlier in the skill acquisition and retention sessions.

We have developed a virtual reality (VR) and an augmented reality (AR) dental training simulator utilizing a haptic device. The simulators utilize volumetric force feedback computation and real time modification of the volumetric data. They include a virtual mirror to facilitate indirect vision during a simulated operation. The AR environment allows students to practice surgery in correct postures by combining the 3D tooth and tool models with the real-world view and displaying the result through a video see-through head-mounted display (HMD). Preliminary results from an initial evaluation show that the system is a promising tool to supplement dental training and that there are advantages of the AR over the VR approach.

 We present a methodology for modelling population dynamics with formal means of computer science. This allows unambiguous description of systems and application of analysis tools such as simulators and model checkers. In particular, the dynamics of a population of Aedes albopictus (a species of mosquito) and its modelling with the Stochastic Calculus of Looping Sequences (Stochastic CLS) are considered. The use of Stochastic CLS to model population dynamics requires an extension which allows environmental events (such as changes in the temperature and rainfalls) to be taken into account. A simulator for the constructed model is developed via translation into the specification language Maude, and used to compare the dynamics obtained from the model with real data.

 Objectives

The goal of dental education is to guide students’ development through different stages from novice to competent, eventually resulting in an expert clinician. In this study we sought to identify process and outcome measures of clinical skill performance by comparing novices and experts using a virtual reality (VR) simulation system developed by our group.

Dental students devote several years to the acquisition of sufficient psychomotor skills to prepare them for entry-level dental practice. Traditional methods of dental surgical skills training and assessment are being challenged by the complications such as the lack of real-world cases, unavailability of expert supervision and the subjective manner of surgical skills assessment. To overcome these challenges, we developed a dental training system that provides a VR environment with a haptic device for dental students to practice tooth preparation procedures. The system monitors important features of the procedure, objectively assesses the quality of the performed procedure using hidden Markov models, and provides objective feedback on the user’s performance for each stage in the procedure. Important features for characterizing the quality of the procedure were identified based on interviews with experienced dentists. We evaluated the accuracy of the skill assessment with data collected from novice dental students as well as experienced dentists. We also evaluated the quality of the system’s feedback by asking a dental expert for comments. The experimental results show high accuracy in classifying users into novice and expert, and the evaluation indicated a high acceptance rate for the generated feedback.

Traditional methods of dental surgical skills training and assessment are being challenged by complications such as unavailability of expert supervision and the subjective manner of surgical skills assessment. This paper presents a dental surgical skills training system that provides a virtual reality environment with a haptic device for dental students to practice tooth preparation procedures. The system monitors important features of the procedures, objectively assesses the quality of the performed procedure and provides objective feedback on the user’s performance for each stage in the procedure. We evaluated the accuracy of the skill assessment with data collected from novice dental students as well as experienced dentists. The experimental results show high accuracy in classifying users into novice and expert. The evaluation of the system’s generated feedback also indicated a high acceptance rate.