电子商务已成为Internet的重要应用之一。然而，随着用户数量的增加和服 务类型的多样化，电子商务系统愈来愈庞大、愈来愈复杂，这使得电子商务系 统的设计和分析更加困难。一般情况下，电子商务系统的需求规范采用非形式 化方式描述，且这种描述具有二义性。本文应用形式化方法对电子商务系统进 行模拟与验证，能够为系统设计者提供一种既明确又便于理解和掌握的系统整 体架构，帮助设计者查找系统设计中的漏洞或缺陷，验证系统的活性、安全性、 公平性和正确性等动态行为性质，使其更加规范、有效、合理、因此，本文的 研究工作具有重要的理论价值和实际意义。 本文在对大量现有电子商务系统形式化方法分析的基础上，根据电子商务 系统的具体特点，综合应用Petri网、时序逻辑、工作流等分析技术，提出并研 究了用于电子商务系统时序性质分析的时序(高级)Petri网方法、批处理功能 及传值不确定性分析的逻辑工作流网方法、实时性质分析的逻辑时间工作流网 方法和主体责任与证据分析的标注工作流网方法。同时，从理论上研究了这些 方法的主要性质，得到一系列重要结果。通过对案例分析，例证了它们在电子 商务系统分析中的应用价值。 目前，国内外可应用于电子商务系统形式描述与验证的方法主要分为四大 类：一般形式化方法、基于逻辑的形式化方法、基于Petri网的形式化方法和基 于工作流网的形式化方法。它们为电子商务的发展和应用起了重要的促进作用。 本文综合分析了它们的特点和缺陷，并在它们的启发下，提出并研究了几种用 于电子商务系统不同性质形式化分析的有效方法。与现有电子商务系统形式化 方法相比较，本文工作的主要贡献表现在如下几个方面： (1)首次将时序Petri网应用于电子商务系统的时序性质分析，且提出并 研究了时序高级(有色、谓词/变迁)Petri网分析技术。以网上证券交易系统为 例，具体例证了时序Petri网和时序高级Petri网模拟与验证技术在电子商务系 统中的应用价值，并基于它的Petri网模型，分析了证券交易系统的时序性质和 功能正确性。 (2)电子商务系统中的批处理功能，涉及传值不确定性。在电子商务系统 批处理功能及传值不确定性形式化分析技术研究方面，本文工作具有一定突破。 本文提出的逻辑工作流网分析技术，既能描述与分析电子商务系统的一般性质， 又能够极好地模拟与验证电子商务系统的批处理功能和传值不确定性。 (3)传统的实时协同系统分析方法，不能明确描述与验证系统的批处理功 能和传值不确定性。本文提出的逻辑时间工作流网，既能分析电子商务系统的 实时性质，叉能描述与验证系统的批处理功能及传值不确定性。 (4)在电子商务系统主体责任、不可否认性及证据的形式化表达与分析方 面，本文克服形式语言方法过于抽象、不便于设计者理解等缺点，提出并研究 了标注工作流网分析技术。它能够充分利用Petri网的动态可视特性和工作流网 的完善分析技术，明确描述和分析电子商务系统中的主体责任、不可否认性与 证据。同时，我们将无阻塞理论引入标注工作流网中，使工作流网的模拟与分 析能力进一步增强，其健壮性分析技术更加完善。 关键词：电子商务系统，实时性质，安全性，时序性质，批处理，传值不确定 性，责任，证据，模型检查，验证，Petri网，时序逻辑，工作流。