摘要： User manual designers generally use written procedures, figures, and illustrations to convey procedural information to end users. However, ensuring that the instructions are accurate and unambiguous is difficult. With respect to accuracy, describing the task and under what conditions it should be conducted can be complicated by considerations such as the ordering of actions within a higher level task and the context under which tasks and lower level actions can be initiated, repeated, and completed. With respect to ambiguity, component and task level issues occur such as which portion of a component is relevant and what context constrains activity. To support accuracy and to decrease ambiguity, we propose a model-based approach coupled with model checking and visualization to aid in user manual development. Our approach integrates formal task-analytic and device models with safety specifications into a computational framework. We demonstrate the value of this approach using alarm troubleshooting instructions from the patient user manual of a left ventricular assist device. By encoding a formal task model, we revealed potential problems with task and device descriptions in the troubleshooting instructions. We also applied linear temporal logic and symbolic model checking to identify issues with the order of troubleshooting steps. Our framework provides insights into the use of formal methods for patient user manual evaluation.