在世界各地的司法改革中,信息系统已成为司法部门组织和管理司法业务流程的关键技术,藉以改善司法信息资源共享及提升司法服务效率。当司法信息系统的执行流程,即司法工作流不满足乃至违反司法制度要求时,将会降低司法服务质量及效率,继而令司法部门陷入失信危机。为此,利用司法信息系统来协调及管理司法流程时需确保司法工作流的正确性和可信性,如确保司法工作流的执行符合法律法规和实践规则、司法工作流所需数据的完整性和安全性。司法信息系统的工作流本质上是很复杂的,也很难被正确地设计。司法工作流涉及不同的参与者（人、数字系统和物理系统）之间的交互,对安全性和隐私性具有较高的要求,还需应对需求与环境的变化。这使得对定义、理解、分析司法工作流变得很困难,且难以保证司法工作流的正确性和可信性。为此,本文研究建立了一种对司法工作流建模和分析的方法,通过构建不同抽象级别和不同形式化程度的工作流模型来定义、理解和分析司法工作流,以保证司法工作流的正确性和可信性。围绕着对司法工作流的建模和分析,本文的主要研究工作如下:研究建立了一个对司法工作流建模和分析的方法。该方法从非正式的用例建模开始,并逐步转向形式化的通信顺序进程（Communicating Sequential Process,CSP）建模。为了将用例转换为CSP模型,该方法先将用例转换为更正式的序列图,再将序列图组合为一个结构图。结构图中的每个序列图都被定义为一个CSP进程,整个结构图也被定义为一个CSP进程,利用CSP的组合语义集成序列图和结构图,得到一个完整的形式化的工作流模型。基于CSP的工作流模型,利用PAT工具验证模型定义的工作流的性质。为验证该建模方法的有效性,以构建我国民事诉讼的工作流为例对该方法进行了说明。用例驱动的建模方法可以将复杂的工作流分解为多个用例,用例可以被独立建模、分析和理解,经过细化和组合技术最终可以得到一个形式化的工作流模型。这种分解和组合的建模方法不仅可以应对复杂的工作流建模,还可以适应业务变化带来的工作流模型的变更。研究利用UML类图和契约描述工作流中操作行为的细节。首先,通过对用例分析,识别和捕获用例中涉及的数据概念,将它们定义为UML类图。其次,为详细地分析工作流中操作需要的数据,定义了一个非形式化的契约来规范和明确工作流中操作的数据需求和行为需求。该契约定义了操作所需的输入数据、输出数据、前置条件和后置条件,可以明确和规范工作流中操作的数据以及行为需求,对于工作流的实现具有很好的指导作用。基于本文的工作流模型理论,设计和开发了一个基于Web的可视化建模工具。该工具提供可视化建模、模型管理、模型转换和模型信息校验的功能,有助于提高建模效率。