知识丨航空机载嵌入式控制软件需求建模的形式化工程方法

关键词：软件需求建模；需求确认；形式化工程方法；形式化方法

嵌入式控制软件广泛应用于现代轨道交通、航空和航天系统等安全攸关系统。以飞机的航空发动机控制系统为例，其控制行为的安全性和可靠性等都依赖于自身的嵌入式控制软件。正是因为如此，确保其嵌入式控制软件的正确性就显得尤为重要。

需求规约是整个软件开发、测试验证与维护的基础。经过长期研究与实践，工业界与学术界均意识到，采用形式化方法精确地描述软件需求，并确认其充分而准确地反映了人们对软件功能和运行场景的预期，是一种从源头确保软件质量的重要手段。尽管形式化方法对保证软件可信性展示了令人鼓舞的前景，然而，在当前的嵌入式控制软件开发领域，例如航空航天领域和轨道交通领域，形式化方法的实际应用仍是一个巨大的挑战，大量深层次的问题有待解决。首先，工业界软件开发人员缺乏针对其领域的需求描述语言。其次，形式化规约的构建过程缺乏系统化的工程方法支撑，如何从原始的、不完备的、非形式化的需求描述出发，逐步建立形式化规约，对于多数工程人员仍然十分困难。再次，形式化规约的需求确认方法尚有局限性。需求确认通常侧重于检查需求描述是否充分且准确反映了用户对软件功能的期望［１，２］。当前在工业界常用的需求确认方法主要是需求文档的审查［３５］，学术界提出的其他方法包括规约的测试和动画［６］等。但是，这些方法缺乏严谨性和系统性，特别是缺乏和形式化理论的有机融合，使得需求确认的效果往往不如人意。

因此，构建一种以形式化理论为科学依据的工程方法，引导工程人员从原始需求出发逐步完成形式化规约构建，且能有效地确认规约充分而准确地刻画了人们对软件功能的期望，对于工业界来说有着重要意义。

为此，我们以航空领域为典型应用领域并与中国航空商用发动机有限公司合作，提出了一种嵌入式控制软件的形式化工程建模方法ＡＣＳＤＬ－ＭＶ（ＡｅｒｏＣｏｎｔｒｏｌＳｏｆｔｗａｒｅＤｅｓｃｒｉｐｔｉｏｎＬａｎｇｕａｇｅｂａｓｅｄＭｏｄｅｌｉｎｇａｎｄＶａｌｉｄａｔｉｏｎ），引导嵌入式控制软件的形式化规约构建和需求确认。具体研究内容包括：（１）设计一种形式化工程建模方法，支持从自然语言需求向形式化需求模型演化的建模过程：需求规约经过非形式化、半形式化阶段，最终演化为形式化规约，并定制开发了一种面向航空领域的轻量级形式化描述语言ＡＣＳＤＬ（ＡｅｒｏＣｏｎｔｒｏｌＳｏｆｔｗａｒｅＤｅｓｃｒｉｐｔｉｏｎＬａｎｇｕａｇｅ），用于对软件功能进行形式化描述。（２）提供一种结合了基于图形的规约审查技术和基于模型的动态执行技术的规约确认方法，从形式化需求规约中抽取变量依赖关系和模式迁移关系并以图形呈现，辅助分析人员进行需求审查；根据需求生成的模型来模拟发动机的运行情况，并与实际运行情况做对比，以判断规约是否与期望的场景一致。

本文的其余部分安排如下：第２节介绍了需求验证领域主要研究现状。第３节介绍了该需求确认方法的整体框架。第４节和第５节详细阐述了方法的关键技术。第６节对该方法在工业实践中的实验与结果进行分析评估。第７节对本文进行总结，并给出了未来的研究方向。

经典的形式化语言和相应的建模方法有Ｚ方法［７］、Ｂ方法［８］和Ｅｖｅｎｔ－Ｂ方法［９］等，均在软件工程领域具有较大的影响力。然而，对于大型的嵌入式控制软件的形式化规约的构建，工程人员难以达到灵活运用传统方法所需的理论基础。为此，Ｌｉｕ等人［１０１２］提出了形式化工程方法的概念，通过提供一种工程化的方法引导开发者将原始需求演化至形式化规约，在不同的软件领域已取得了良好的效果。然而，在嵌入式控制软件领域的建模，类似方法仍然是匮乏的。

规约审查是需求验证的一种经典技术。文献［５］提出了一种基于查询模型概念的方法，以验证需求规约是否满足给定的需求，通过提出场景问题并分析结果，用以验证需求。文献［４］引入了一个心理模型作为需求验证的基础，并按照特定的标准进行审查。文献［１３］给出了一种基于虚拟模型的规约审查方法，需求规约被转化成用于结构和功能审查的虚拟原型。然而，在实际实践中，当规约规模大且逻辑复杂时，人工审查规约的功能描述通常难以取得预期的效果。因此，本文给出了一种基于图形的审查策略。

规约仿真也同样用于需求验证，它包括模型检查和规约执行。ＰｒｏＢ是Ｂ形式规约的验证工具集，通过显示其状态转换路径来仿真执行其反例［１４，１５］。ＵＰＰＡＡＬ也通过模型检查来仿真执行目标系统的动态行为［１６１８］，它允许系统使用状态和转换建模，并自动探索状态空间。文献［６］给出了一种基于仿真的检查方法，该方法使用仿真来指导检查过程。通过展示所选功能中常见的输入和输出之间的关系，可以提高检查活动的效率。从实践角度来说，仿真更接近于一种设计层面的验证，而非针对需求分析。

规约测试是另一种重要的需求验证技术。文献［１９］提出了一个使用动态切片技术来测试软件设计规约的工具。文献［２０］使用测试模块来测试形式化规约，这些测试模块以与形式化规约相同的形式来描述，并可以自动生成。文献［２１］给出了一种用于审查目标形式化规约的任务树的规约测试方法。它针对不同类型的审查任务树，采用不同的策略来生成测试用例。本文借鉴了对规约进行测试的思想，测试用例根据航空领域ＤＯ－３３３标准所要求的ＭＣ／ＤＣ（ＭｏｄｉｆｉｅｄＣｏｎｄｉｔｉｏｎ／ＤｅｃｉｓｉｏｎＣｏｖｅｒａｇｅ）覆盖准则来生成，此测试用例生成过程本身将有助于发现规约中潜在的表达式描述错误与缺陷。

在轨道交通领域，文献［２２２４］用形式化的方法对列车控制软件进行了需求确认。工业界常用ＳＣＡＤＥ（ＳｏｆｔｙＣｒｉｔｉｃａｌＡｐｐｌｉｃａｔｉｏｎＤｅｖｅｌｏｐｍｅｎｔＥｎｖｉｒｏｎｍｅｎｔ）平台进行规约的验证确认［２１］，其核心方法是采用状态图描述需求，并通过形式化验证检查模型的一致性。但是，ＳＣＡＤＥ本身对建模方法并没有明确的引导和约束，尚未做到形式化方法与软件工程的合理融合。在航空电子领域，ＲＳＭＬ（ＲｏｏｔＳｙｓｔｅｍＭａｒｋｕｐＬａｎｇｕａｇｅ）［２５］语言使用ｓｔａｔｅｃｈａｒｔ风格的符号体系对需求进行建模，但与ＳＣＡＤＥ类似，对于工程人员来说，并不适合作为原始建模工具，更适合设计阶段。

综上所述，无论是学术界还是工业界，尚缺乏成熟的形式化规约构建方法。

ＡＣＳＤＬ－ＭＶ方法包含需求建模和需求确认２个阶段。该方法的整体框架如图１所示。

建模阶段从建立以自然语言撰写的非形式化需求文档开始。由于自然语言描述存在显而易见的二义性和模糊性，我们将其转换为更精确的半形式化需求模型。规定半形式化需求文档中，任何数据结构必须是形式化定义的，即变量的数据类型被精确描述。而变量之间的关系可以仍然是非形式化的。半形式化需求模型主要基于工程上可行性的考虑。从软件工程的角度来说，建模者对软件功能的理解往往是伴随着文档撰写而逐渐清晰，因此文档必然需要多次变更修改。如果直接撰写形式化需求，不仅技术上困难，其变更也会带来巨大的时间和成本损失。反之，我们提供半形式化需求阶段，建模者只需要先关注变量的数据结构特征，而暂时以自然语言表述其关联关系，待建模者确认需求文档确实已经充分描述了功能以后，再将其向完全形式化模型转化。在此过程中，即使系统功能发生变化，其修改的代价也是可以接受的。另一方面，当数据结构清晰之后，需求分析者对于功能的理解也随之深入，更有利于撰写需求规约。最终，工程人员可以把半形式化规约演化为形式化规约。为了有效刻画航空发动机的嵌入式控制软件需求，我们提出了一种轻量级的形式化建模语言ＡＣＳ－ＤＬ，用于撰写最终的形式化需求规约。ＡＣＳＤＬ对于控制软件有良好的描述能力，包括支持时间周期等诸多领域特征。

在需求模型构建完成之后，需求分析者和软件开发人员主要关心的问题是模型是否真实、完整地体现了人们对软件功能和性能的预期。需求确认阶段包含了２种主要确认方式：静态需求审查和动态模拟执行。为了实现自动化需求验证，需求规约需要被处理为可执行模型，即可执行的软件原型，从而生成用于审查的图形并进行基于场景的规约测试。根据与航空发动机领域的工程师的交流，在软件需求描述层面，工程人员最关心的是涉及到安全攸关功能的变量是否被正确定义，比如发动机转速这个变量，在实际运行中非常重要。由此，我们从软件原型生成了变量依赖关系图，描述了一个变量的取值是否受其他变量的影响，刻画的是变量之间的交互关系。但是，仅仅从静态分析层面对需求进行分析是不够充分的，因为未能确认需求规约是否能正确描述预期的物理运行场景。为此，我们动态执行了从需求文档转化而成的模型，并将运行结果与合作方的Ｍａｔｌａｂ仿真结果进行了对比，以此来判断需求规约是否满足预期的实际物理场景。经过静态审查和动态测试，控制软件的需求规约可以得到充分的确认分析。

形式化规约构建过程的目的在于将原始的、不完整且模糊的需求，通过工程化的手段，逐步演化为最终精确的、逻辑正确且无二义性的形式化需求文档。其起点是自然语言描述，而终点则是用形式化语言描述的需求文档。在给出详细的形式化规约构建技术之前，我们首先对所提出的形式化语言ＡＣＳＤＬ给出具体的定义与解释。此形式化定义与解释的一致性、完备性、正确性证明篇幅较长，又因本文是形式化方法的工程运用，所以不做展开。ＡＣＳＤＬ所描述的航空发动机的需求模型的形式化描述如下所示：

对于嵌入式控制软件来说，在软件的起步阶段，需求撰写人员对系统的预期功能尚不明确，而且参与系统分析的人员背景不同，因此采用自然语言的需求撰写方式是比较合理有效的。嵌入式控制软件的非形式化需求包含系统功能和相关性指标，主要包含３部分：功能描述、数据定义和约束条件。

如图２展示了一段非形式化的软件需求。该功能模块是“ＫＰＭ信号”，表示在不同状况下如何改变ＫＰＭ信号的状态。比如，需要通过对发动机所处的状态进行判断来修改ＫＰＭ信号的值。这样的需求文档便于发动机工程师和软件工程师沟 通和阅读，然而其对需求的刻画显然是不够精确的，因为变量的类型等因素还未确定，需要工程人 员提供更进一步的定义。

半形式化需求是对数据结构或系统结构等易于形式化的系统特征进行精确描述，而具体功能的描述仍然以自然语言描述为主。这样的需求文档可视为形式化和非形式化需求描述的一种平衡，既便于程序开发者理解需求，也便于需求分析者检查文档。对于嵌入式控制软件来说，半形式化文档侧重于对数据结构的形式化定义。半形式化需求是在工程中为了帮助需求撰写人员快速理解、掌握形式化需求描述的辅助阶段，重点在于帮助需求撰写人员建立形式化文档的概念。在工程运用过程中，我们会帮助需求撰写人员了解并掌握半形式化以及形式化需求文档的撰写方法和规范，以免出现理解上的差异。在熟练掌握撰写形式化需求之后，需求撰写人员可直接将原始需求文档转化成形式化需求文档。半形式化文档应满足以下特征：（１）所有变量和常量的数据结构和类型应形式化描述；（２）功能被结构化定义，即每个功能都有明确的输入和输出变量；（３）每个功能的输入输出变量之间的关系仍可以保留为非形式化。由于规约本身没有完全形式化，其修改的代价相对可控。图３展示了图２所示功能的部分半形式化描述。

在半形式化文档中，每个变量的数据结构都有详细的定义。例如，变量“ＫＰＭ信号”的类型是布尔型，ＫＰＭ信号如何变化则仍是用自然语言描述的。在半形式化阶段，即使需求发生变更或修改，其代价仍在可承受范围之内。而随着对变量数据结构的精确描述，需求分析者对系统功能会有更清晰的认识。

在完成了对半形式化文档的检查之后，工程人员可以采用ＡＣＳＤＬ语言将规约完全形式化，即通过ＡＣＳＤＬ语言将每个功能输入和输出变量之间的关系予以精确化定义，并将所有全局约束条件等予以形式化定义。图４展示了图２所示功能的形式化描述。

一般来说，构建形式化描述的过程，对工程人员来说是促使他们对需求内涵进行思考的过程。一些模糊的需求在这个过程中被逐步明晰。例如，对于有二义性的需求，可以在此过程中逐渐暴露，如图５所示。

那么在计算任务执行３０ｓ时，是增加１ｓ还是３ｓ的执行时间就产生了语义上的二义性。而在进行需求的形式化规约构建时就可以发现并解决这一类问题。

在实际的需求撰写中，因为需求规约是工程人员手工编写的，因此不可避免地会出现语法错误和逻辑错误。为了实现自动化的需求审查，我们需要将这些错误排除，并将其转化为机器可识别并且可执行的模型。为了生成可执行模型，需要先根据ＡＣＳＤＬ语法的定义，将形式化需求文档抽取并解析成抽象语法树结构的控制流图ＣＦＧ（ＣｏｎｔｒｏｌＦｌｏｗＧｒａｐｈ），再把ＣＦＧ作为输入，通过函数转化成可执行的软件模型。

由于模型是对需求文档的内容进行抽取分析而来的，因此模型的各个组成部分与需求规约的抽象解释是一一对应的。我们使用了Ａｎｔｌｒ工具对自定义的需求规约文法进行分析生成语法解析器，再使用语法解析器对Ｗｏｒｄ文档进行分析生成语法树并转化成可执行模型。

该模型由模式流（ＭｏｄｅＦｌｏｗ）、模块（Ｍｏｄｕｌｅ）和数据字典（ＤａｔａＤｉｃｔｉｏｎａｒｙ）３部分组成。

模式流描述了嵌入式系统的整体运行框架。模式流由模式及模式间的迁移条件组成。在嵌入式系统中，系统从初始状态开始，不断地执行周期性任务，直到满足向其它状态迁移的条件，然后发生状态的转换。对于系统而言，状态是非常关键的全局元素。我们把状态抽象成“模式”，剔除了那些非重点的状态，帮助工程人员找到需要关注的核心状态。在每个模式中，都有多个周期长度不同的周期任务，每个周期任务中包含一个控制流，控制流是由ｉｆ－ｅｌｓｅ结构或ｗｈｉｌｅ结构等控制逻辑以及模块等计算任务组合而成的。如果该嵌入式系统比较复杂，比如模式之间具有层次关系，那么我们也可以通过在模式中加入子模式，再将子模式间的执行逻辑进行处理来对具有层次化结构的系统行为进行描述。

模块是具体的计算任务。在航空领域有一些常见的计算任务，比如发动机的控制系统需要以当前所处高度、温度等外部数据作为输入来计算发动机需要提供的推力大小，并通过阀门来进行油量控制。不同的计算任务之间耦合性较小，通常在模式的控制流中被调用。

数据字典包含了整个需求文档中定义的变量。数据字典记录了变量的名称、类型、初始值、最大值和最小值等信息。每个模块中都会使用或修改部分变量来完成相应的计算任务。

图６展示了ＡＣＳＤＬ模型的３个层次。最左层展示了各个模式之间的迁移关系，中间层展示了模式中的控制流，最右层展示了具体的计算任务，即模块。

最左层可以帮助工程人员把握整个系统的框架，中间层可以帮助工程人员判断控制流是否符合预期，最右层则是数据和逻辑的综合处理。在最左层中有３个模式，模式之间通过有向箭头来连接。如果模式之间有迁移关系，那么就会有一根有向箭头。中间层是某个模式的某个任务的控制流，描述了具体的控制规律。在最右层，每个模块代表了不同的计算任务，每个计算任务实现了发动机控制中的一个小功能。

（１）基于图形的需求规约审查。

根据从工业界调查了解到的信息，为了更好地帮助工程人员发现需求中的问题，我们针对变量和模式流建立了２种关系图：变量之间的影响关系和模式之间的迁移关系。为了更直观地进行观察，我们将这２种关系使用变量影响关系图和模式迁移关系图进行表达。

变量影响关系图用节点表示不同的变量，用箭头表示变量间的影响关系，箭头指向被影响的变量。箭头上标注的条件表示特定条件下的变量直接影响关系。而模式迁移关系图用节点表示不同的模式，用箭头表示模式间的迁移关系，箭头指向要迁移到的模式。箭头上标注的条件表示特定条件下的迁移关系。工具可以从原型中自动提取上述变量影响关系图和模式迁移关系图。

通过对ＡＣＳＤＬ模型中每一个模块的遍历定位到赋值语句所在的位置，然后提取出赋值语句中的左值与右值，生成变量影响关系对，并判定赋值语句中的右值对左值有直接影响关系。当赋值语句出现在条件语句中时，对判断条件进行存储，并判定赋值语句的右值在该条件下有对左值有直接影响关系。存储的变量影响关系对用于生成变量影响关系图。对于每个待观察的变量都可以生成上述图表，并根据图表判断其生成是否符合预期的输出。

通过对ＡＣＳＤＬ模型中模式流的遍历，分析每个模式向外迁移的条件及目标模式，可生成模式迁移关系图。

如图７所示是ｘｘ模块中ｘｘ变量的影响关系图，图中过长的条件都被设置成了“ｃｏｎｄｉｔｉｏｎ”字符串，如果要查看具体的条件，可以点击“ｃｏｎｄｉｔｉｏｎ”弹出消息框。由图７可知，Ｃ变量由ＥＳ＿Ｍ变量及ＥＳ变量直接影响，其中，ＥＳ变量在ｃｏｎｄｉｔｉｏｎ条件下对Ｃ变量有影响关系。

通过与航空发动机公司的合作，我们对其发动机控制软件的系统进行了分析总结，得到了包含１０个模式的模式流图，也代表了ＡＣＳＤＬ模型最上层的具体实例，如图８所示。因为保密的原因，隐去了具体的模式名称，迁移关系的条件也用字符串“ｃｏｎｄｉｔｉｏｎ”代替了。

（２）基于模型的测试用例生成。

在航空领域中对测试用例的覆盖准则有严格的要求，测试用例需要满足ＤＯ－３３３标准：测试用例需满足ＭＣ／ＤＣ覆盖准则的要求。根据ＤＯ－３３３认证标准的要求，我们提出根据形式化需求自动生成符合ＭＣ／ＤＣ覆盖准则的测试用例，并辅以真值表帮助人工检查生成测试用例的正确性。该方法还可以帮助发现模型本身的一些错误。生成满足ＭＣ／ＤＣ覆盖准则的测试用例的方法针对的是模型中的每个模块。对于模块中的计算逻辑，通过算法收集满足ＭＣ／ＤＣ覆盖准则的约束并将其输入Ｚ３约束求解器中求解来得到测试用例。

如图９展示了一个条件错误的示例：

通过对该例子进行基于ＭＣ／ＤＣ覆盖准则的测试用例约束与求解，可以得到如表１所示的结果。

表１中空白的一项因为条件约束有错，无法求出测试用例。在模型检查的过程中，根据ＭＣ／ＤＣ覆盖准则生成测试用例，如果有无法生成测试用例的情况，那么就代表模型中的控制算法有错，说明原需求文档的控制逻辑有误。

（３）需求模型动态确认。

本文运用仿真这种模型动态确认方法来验证模型的正确性。软件测试不能证明被测试的软件是正确的，只能找到被测试对象的错误。类似地，仿真也无法说明软件模型是正确的，但是如果仿真的过程中发现与实际情况不一致，那么软件模型就一定有问题。控制工程师给定的物理环境模拟器是一个确定性系统，即给定相同的输入序列，必然得到同样的输出序列。在此假设下获得可执行程序的方法的模拟结果。模拟执行示意图如图１０所示。

模拟仿真的过程是：首先进行初始化，为全局变量设置初值，为各个基本模式的计算过程创建相应的任务，启动物理环境模拟器；然后进入控制回路。在该回路中，首先调用物理环境模拟器的接口，从环境采集数据，更新输入变量；然后执行当前模式相对应的计算任务，计算任务由一系列模块组成。如果计算任务完成，则开始检查模式切换条件，调用物理环境模拟器的接口驱动执行机构，然后进入下一次迭代。如果计算任务因为超时被挂起，则调用物理环境模拟器的接口驱动执行机构，然后进入下一次迭代，直接继续未完成的执行计算任务。其整体流程如图１１所示。

为了验证本文方法的可行性并展示其有效性，我们将其应用到真实的航空发动机控制软件的需求分析中。实验中有２名经验丰富的工程师全程参与。在将非形式化需求逐步转化成形式化规约的过程中，因为工程师对领域知识非常熟悉，需求规约的构建大约用时２个月。该控制软件的形式化需求规约是一份包含了１０个模式、１５２个模块、１１４５个变量的ＭｉｃｒｏｓｏｆｔＷｏｒｄ文件。

在规约转化成原型的过程中，一共发现了７８个语法错误、７２个变量遗漏、２３个变量类型错误。在进行图形化审查时，一共生成了１５２个变量依赖关系图、１５２个变量模块依赖关系图、１５２个模块模式依赖关系图、１个模式迁移关系图。另外，通过对需求模型的分析，一共生成２３４２条基于ＭＣ／ＤＣ覆盖准则的测试用例。通过合作方提供的外部数据，我们顺利完成了需求模型的模拟执行，与合作方通过Ｍａｔｌａｂ模拟的情况一致。

另外，针对模式流中的迁移关系，我们还进行了互斥性的验证。如果某个模式有多个迁移条件，对它们做与操作，并通过Ｚ３求解器对其求解，如果有解，那么该模式的迁移条件不满足互斥性。比如条件ＰＬＡ．ＢＩＴＳｅｔＴｉｍｅ＝＝ｆａｌｓｅ与ＰＬＡ．ＳｅｌｆＦｌｔ＝＝ｔｒｕｅ，它们就不满足互斥性。

在形式化需求规约确认的过程中，我们共发现了３个原始需求的错误。

如图１２所示是一段需求文档，这是一个需求描述不充分的错误，是在进行形式化规约构建的过程中发现的。

如图１３所示是发动机转速的仿真图。这是一个条件遗失的错误，是在仿真的过程中发现的。本文的仿真结果与合作方在Ｍａｔｌａｂ上的仿真结果在大约３００周期的时刻发生了偏差。通过分析发现是我们在编写形式化需求的过程中，相比原版需求文档，一个模式的某个迁移条件漏写了，所以仿真结果不一致。在修改了这个错误之后，我们和合作方在Ｍａｔｌａｂ上的仿真结果是一致的。

本文提出了一种面向航空领域的嵌入式控制软件需求建模形式化工程方法ＡＣＳＤＬ－ＭＶ，包含了演化形式化规约构建和需求规约确认２大阶段。演化式建模方法通过系统化的过程控制，引导需求分析人员建立非形式化需求规约、半形式化需求规约并最终完成形式化规约。需求确认用以检查需求分析人员撰写的形式化规约是否真实、充分地刻画了预期的功能和运行场景。实验结果表明，该方法具有良好的可用性，并在实际航空发动机软件开发项目中展现了优于工业界传统手工审查方法的缺陷发现能力和提供了直观地展示需求中变量关系的能力。

未来进一步的工作将围绕深入研究自然语言处理技术和优化规约测试２个方面展开，并最终为每个领域构建完整的需求建模环境与工具。具体来说，我们将进一步探索自然语言处理技术与需求建模活动相结合的方法，比如说通过自然语言的方法将需求文档转化成半形式化乃至形式化的需求模型，尽可能将需求规约撰写中的人为因素和主观因素降低，以减少需求规约潜在的缺陷和错误，并提高建模效率。而基于场景的规约测试，我们将进一步分析场景构建的准则和科学依据，建立相应的场景构建规则，最终实现更为系统化、更能被工业界工程人员接受的嵌入式控制软件形式化规约构建方法和工具链。

文章选自《计算机工程与科学》，作者：黄怿豪，冯劲草，郑寒月，缪炜恺，蒲戈光，作者单位：（华东师范大学上海市高可信重点实验室，上海 ２０００６２），转载此文章仅以传播知识为目的，如有任何版权问题请及时联系我们！