10企业内控实施方法研究基于领域分析与形式化

企业内控信息化实施的规范化方法研究基于领域分析与形式化方法欧阳电平(大学经济与管理学院【 】企业内控信息化实施需要运用 将内控理念、 控制制度规范、流程、措施到信息系统中，将企业信息系统转化、提升为一个集成了企业内控需求的信息化管理平台。企业内控信息化实施是一个复杂庞大的系统工程，需要有科学规范的方法、工具和技术以保证内控系统实施的质量。领域分析和形式化方法是计算机软件工程中对软硬件系统进行分析、规范、建模、证明的方法和技术，将其应用于企业内控信息化实施，可以在内控系统运行前，通过基于数理逻辑证明的方法快速有效地发现系统设计和实施中存在的缺陷和，降低企业内控系统低效或失效的风险。本文以销售业务为例讨论了领域分析与形式化方法的内控信息化实施过程。【 控制信息化实施领域分析形式化方法销售业务内自2002年颁布萨班斯法案后，各国对控制的重视达到了前所未有的高度。2010年国部等五部委联合发布了《企业控制基》、《企业控制配套指引，标志着适合国企业的 控制规范体系已基本建成尽管 控制理论和制度规范建设取得了巨大进步，企 控制系统成本高昂、效率低下、失败率居高不下、成功经验难以移植等”( 7)。关于如何将 控制理论及其成果应用于企业 控制的实践，提高 控制的实施效果，人们从公司治理、理论完善、执行机制、评价与信息披露、信息系统多个视角展开了研究，但从科学规范的实施方法和技术的角度进行研究的则不多。信息化是世界发展的必然趋势， 控制信息化已成为一种必然的和途径，企业可以通过信息化将内控理念和规范的 控制制度、控制措施到信息系统中，以实现 基础的人工与T控制

相结合的方式，其实施过程是一个复杂庞大的系统工程，涉及到治理结构、管理基础、员工素质、T应用基础等诸如能从实践的角度利用科学的去理论研究的成果，将是 控制理论到实践的有益的补充”( 和 7)。本文主要从科学、规范的方法和技术的视角，探讨将计算机软件工程学的领域分析和形式化方法应用到基于T的 控制系统的设计与实施，为环境企业 控制理论与实践的相互有效转化探寻一种新的实施思路与规范的技术。一、领域分析和形式化方法是计算机软件工程中对软硬件系统进行分析、规范、建模、开发、证明的方法。计算机软件工程经过多年的发展取得了巨大的进步，开发方法开发工具和技术不断推陈出新，领域分析与形式化方法及其开发工具和技术也是多种多样。依据企业 控制领域分析复杂度高等特征，本研究选取了适合描述复杂系统的领域分析中的B方法，和能自动进行推导证明的形式(一)领域分析 领域分析也称领域工程分析，是指运用领域分析方法和工具，针对一个计算机应用领域进行需求分析，识别、提炼并抽象出该应用系统的共同特征和区别出其可变特征，从而构建领域描述模型:(1)件设计开发或二次开发(系统上线)之前，对应用系统进行详细的需求分析;(2)的可被各个利益相关人理解的方式表述需求，即用某类表达工具建立领域描述模型;(3)的部分以便进行形式规范描述和形化验。本文使用丹麦教授D．nrB方法(r6)。该方法在对一个领域进行分析时，首先要明确这个领域中包含的实体(y)、函数(cn)、(t)和行动序列(r)这四个要素(简称:B方法)。在明确了B，再对该领域的不同切面即子领域进行分析。上述四个要素具体描述如下:实体，指在该领域中，本质静止不变的对象，在实体上可以定义若干关于实体的属性;函数，规定领域中的实体由输入到输出的变化规则;，指可以触发一系列行动序列的函数;行动序列，指的活动序列。(二)形式化方法(Formal统进行分析、规范、建模、开发和验证的方法。它具有精

确无二义性、简洁且机器可证明等优点。目前主要应用于要求高安全性的系统开发中。形式化方法常用的分析方法及其工具主要分为代数规约描述(定理证明)和模型检测两类。本文中研究对象(企业内控系统)本质上说是一个社会系统，由于社会系统的不确定性，使用模型检测方法对状态空间不确定的系统对象进行分析，可能存在状态空间”的问题。因此本文的研究方法及其工具选择了以代数方法为主，同时兼顾了状态空间转换描述的S/J方法。该方法是一种以代数规范语言J为工具，建立在状态观察系统(S:elnm)上的形式化建模分析方法，同时它也是一种基于定理证明的验证方法，能通过J的自动证明系统对模型的性质实现机器自动推导证明，在系统设计初期找出与设计目标不符的设计，从而尽早尽快的发现系统缺陷和，找出修正方法。同时S/J方法的类型描述与领域分析的实体分析方法相对应;S模型中的状态转换规则与动作行为序列对应。由于领域分析描述的系统模型不能精确表达所构建系统的性质以便于机器自动验证，因此，在领域分析基础上，可利用形式化方法对领域分析模型进一步的形式化规范建模和描述，以便对所建的领域模型的性质由计算机进行自动推理验证，以提高系统实施的可靠性和有效性。图1是使用形式化方法进行系统规范和证明的示意图。1(三)领域分析和形式化方法在内控信息化实施中的领域分析和形式化方法已经在数字管理、安全协议证明、电子政务等方面得到了广泛的应用。及丹麦的科研人员已经从数理逻辑的角度对本文使用的领域分析(B)和形式化方法(S/J)及其技术的可靠性进行了数学证明(itl．5)。无论是从理论还是实践方面，领域分析和形式化方法都有良好的应用基础。企业控制是一套风险防范机制，在信息系统环境下，这套风险防范措施是由人工控制(也称一般控制)计算机程序控制(也称应用控制)共同实施，并且控制系统的设计既涉及到组织制度设计又涉及到管理软件的内控功能设计，需要尽快发现设计中的缺陷和。领域分析和形式化方法作为一种成系统分析、开发、建模和验证的规范方法和技术，用于企业内控信息化实施在技术上是可行的。领域分析不需要特殊的应用条件，

计一样，主要是一种专业人员的智力活动，只是需要将分析的成果形成规范化的文字文档。而形式化方法按大分类来说，包括代数方法和模型检测方法(如:ML，fJ)，所要求的计算机软硬件环境并不复杂，分析人员可依据自己对方法和工具的熟练程度进行选择。本文使用的B方法和S/J方法的环境和工具都是开源免费的，可以从J上进行，并且是作者在研究期间主要使用的工具和技术，有相关的研究基础。因此，这类分析和建模工作从具体实施角度来看，企业并不需要增加设备的投入，而人员方面可聘请管理或专业人员)选择自己熟悉的分析工具来完成，仅需付企业内控信息化实施指企业运用信息系统施行企业内部控制的过程，主要包括二个阶段:首先要利用T技术手段将企业的内控理念、制度、流程、措施到信息系统中，将信息系统转化和提升为一个集成了企业 控制需的信息化管理平台; 然后是运用信息化管理平台执行企控制，这是一个长期的实行过程。显然，除了人和体制因素外，控制的需求直接影响 控制执行的效果。在建立信息系统的同时必须考虑、研究和设计内控过程的嵌入，以实现企业业务流程、会计工作流程、信息流程和内控流程的集成”(3)。因此，如何构建一个集成了企业控制需求的信息化管理平台，如何检价所构建 领域分析和形式化方法作为一种科学、规范的实施方法和 (一)能够及早发现管理软件设计中是否存在内控功企业内控信息化实施从技术层面来看，套满足企业 控制需求，整合业务处理流程和控制流程一体的管理软件。从 控制的角度，这套管理软件的开发需要对企业的各个业务循环、各个管理层次的经营风险、控制目标、控制活动、控制措施进行分析，在企业 控制理论和制度规范指导下，将适合于计算机程序控制的制度规范、流程、方法、措施编写成计算机程序嵌入到业务处理程序中，提供一套基于T内控的自动执行机制。计算机对控制最重要的贡献之一是其防止误差进入内控系统的能力，以及如果存在误差就能追踪和及时矫正的能力，而能否发挥这些优点取决于应用系统的开发和设置时有无将相应的功能嵌入系统之中”(7)。然而，要人们用自然语言表达这种集成了内控和业务处理的复杂庞大的管理软件需求而没有缺陷和是很的。领域分析和形式化方法运用的是规范的、基于数理逻辑的分析推理工具和技术，可以在管理软件开发阶段发现软件设计中是否存在 控制功能的缺陷和，防止系统投入使用后的风险，尤其适用于有管控、成本管控等高可信管理软件开发需求的企业。(二) 为ERP系统上线时企业内控措施的嵌入与检验当前，国企业的会计信息系统处于从“信息孤岛”向“系统集成”的期，不少企业已运行或正准备上线ERP系统。企业可以通过商品化软件、自行开发等途径获得ERP软件，建立信息系统。由于ERP软件是一个复杂庞大的管理软件系统，尤其是商品化的ERP软件的考虑通用性功能，企业需要通过二次开发(系统上线)的过程将符合企业需求的控制制度、流程、措施嵌入其中，即在各个业务板块或子系统初始化时正确设置IT控制功能，以便企业的控制制度和措施通过信息系统自动执行。ERP系统上线的过程是一种将人工控制的管理

流程转化成信息流为基础的基于T内控的管理流程的过程，实施者不仅要熟悉整个P软件的内控功能，同时要熟悉企业的控制制度体系、机构设置及权责分配、业务流程的主要风险和关键控制环节、控制措施等诸多业务知识。领域分析和形式化方法能帮助实施者头绪，按照企业控制的需求正确启用P系统中的内控功能模块和控制措施，并检验出企业内控制度设计或P软件中内控功能设计的缺陷。(三)提高企业内控系统实施效率，便于成功经验的企业内控信息化实施首先是要利用IT技术，息系统转化和提升为一个集成了内控需求的信息化管理平台。由于不业、不同企业的组织架构、经营风险、内控目标、业务流程都有不同，企业要根据自身的需求设计和建立基于T的 控制体系，构建满足个性内控需求的信息化管理平台。如果采用传统的手工作坊式”的实施方式，即主要依靠设计与实施者个人(或团队) 的经验和技巧，采用手工作业的方式，使内控理论到内控实践的转化存在太多的人为因素，存在效率低下、质量没有保障等诸多弊端。领域分析和形式化方法提供的规范实施技术可以排除人为因素的影响。通过对纳入 控制范围的控制活动所采用的内控措施分析，分离出哪些可以由计算机程序进行自动控制，哪些还必须由人工控制，哪些可以通过信息化手段完成内控工作; 并且针对不业的各类企业相应的内控需求建立相应的分析和验证模型，可以提高内控信息化实施的规范性; 验证过的内控模型既便于移植，同时也可以作为内外审计部门对企业内控系统的有效性进行评价的依据。(四)为 控制理论与实践之间相互有效转化提供术控制作为企业防范风险，保障企业战略实现的一套制度体系，长期以来，传统的控制方式主要是基于权力制约和岗位分置的人工控制。传统控制比较关注岗位分设、组织设计、管理程序与手续、监督检查方式等内容，并通过这些工作实现控制目标”(6)。经济全球化和广泛深入应用，企业的市场竞争环境越来越复杂多变，对控制系统的有效性要求也越来越高，控制系统规模不断扩大，内容日益复杂，系统的成本不断高涨;同时伴随着的是控制和方法的科学化和现代化，以及控制的信息化。显然，对于这样复杂庞大的企业内控系统设计和实施，仅靠个人的经验和技巧，靠手工作坊式”的实施方式是很难保证质量用规范化的方法和技术进行复杂控制系统的设计和实施，以经济地设计和实施高质量的控制系统并有效”(和7)。计算机软件工程在人们用自然语言表达的内控理念、制度流程、内控措施转化成基于T的内控系统之间架起了桥梁，领域分析和形式化方法能将设计者用自然语言表达的企业控制制度、领域的风险特征和控制措施进行分析，逐步转化成用规范的符号语言表达的计算机能实施的模型，并可以对符号语言描述的内控系统模型的性质进行自动的机器推导，保证所设计实施的基于T的控制系统无二义性，以便有效运行和。领域分析与形式化方法的应用框架如图2所示。企业内控信息化实施的前期工作是要建立一套完整的企业 控制制度体系，形成一本企业 控制手册这既是会计师或审计部门或内审部门对企业 控制系统进行审计的依据，也是内控信息化实施的依据。企业需要专成立项目组或委托专业的内控管理负责内控制度体系的设计。首先需要针对企业管理现状进行诊断，按照内部控制规范对其组织架构、部门设置、部门职责和岗位职责、各个业务板块配套的制度和流程等进行梳理;然后根据内控存在的问题和缺陷提出整改建议;再按照 控制规范和配套指引的要求，根据企业战略目标、经营风险、内控目标业务流程等建立一套完整的适应企业需求的 控制制度体系。企业 控制制度体系的设计必须由专业人员来完成计算机是无法替代的。企 控制制度体系设计完成后，企业内控信息

实施的第一阶段任务是将设计的 控制制度与企业管理信息系统融合。可以运用领域分析和形式化方法将专业人员设计的基于权力制约和岗位分置的 控制制度条例，转化成以信息流为基础的T 控制的规范描述模型，并对模型的内控制度的有效性进行验证，再将规范、有效的制度流程和管控措施嵌入企业信息系统，一般通过管理软件开发或系统上线(二次开发)的途径实现。领域分析与形式化方法在企业内控信息化实施的应用步骤如下:一)运用领域分析方法对企业内控领域进行分析建模领域分析是运用领域分析方法(如EFEB方法)针对企业 控制领域的控制环境、控制活动等要素进行分析找出问题域的范围、目标需求、功能需求、性能需求及限 “由上而下”逐层对各个子领域的内控子系统进行领域分析和描述，并给出上下层级的映射关系;同时提炼出该领域中与内控风险防范紧密联系的实体、函数、动作序列，确定实体的关键属性，定义领域中函数的输入与输出之间的变化规则，以及定义与动作序列的含义在此基础上，运用领域描述工具(自然语言和符号语言)建立能被各个利益相关人接受理解的基于T的内控子系统的领域描述模型(B模型)，提取出与所建模型相关性质的部分，为下一步形式化分析建模提供基础。与其他的系统分析方法相比，领域分析所建的领域描述模型便于转化成形式化规范模型，以利于机器自动验证。2(二)运用形式化方法对企业内控领域描述模型进行在对企业内控领域提炼出基于T的内控系统的领域描述模型的基础上，需要精确、无二义性描述出所建模型的性质，既要能被各利益相关人接受还要易于被机器自动推理验证。因此，需要运用形式化方法及其工具对所建内控系统的领域描述模型相关性质的部分进一步的形式化规范建模和描述，同时要保证领域分析模型与形式化模型

具有可对照性。本文采用OTSCafeOBJ方法，将所建的内部控制系统的领域描述模型转化成状态观测系统(OTS)模型;使用CafeOBJ语言工具对控制系统的OTS模型进行形式化规范描述，以便运用CafeOBJ的自动推理系统对(三)运用形式化推理工具对企业内控系统的形式化在对企业内控系统进行形式化建模和描述的基础上将模型所涉及到的企业 控制规范和企业设计的 控制度的相关条例的自然语言描述，转换成基于数理逻辑的形式化语言的规范描述。这些相关条例作为企业内控系统形式化模型应足的相关性质使用J的自动定理证明器来证明:所建的企业 控制系统的形化模型是否足 控制规和企业设计的 控制制度的关条例。(四)对形式化推理结果进行分析说明，提出所建模结 控制理论和制度规范，解释所建的企业内系统模型推理的结果，对证明过程中发现模型的逻辑，找到关键风险控制点并提供相关的模型改进建议。主要包括如下三个方面: (1)对于能够直接证明的相关内控条例，则证明按照所建 控制系统的模型进行实施，能够满足相应的内控目标; (2)对于能够找到引理(a)证明的相关内控条例，依据推理所得的引理描述，可给所建内控系统模型的相应改进方案与建议;(3)对于形式化模型中不能证明的相关性质，则找出形式化模型中与该性质相关的控制点，表明该内控规则不能通过信息化进行控制，还必须由人工控制，或企业内控制度设计中存在缺陷。

(五)修改完善企业内控系统模型，应用到企业内控将形式化分析的结果与所建的内控系统模型综合分析讨论:模型存在哪些内控缺陷和;相关内控制度和控制措施设计是否合理;能否通过信息化修正并完善;等等。将修改完善后的企业内控系统模型应用到企业控制信息化实践中。四、企业内控信息化的领域分析与形式化建模过程:以销售业务为例(一)领域分析首先需要确定销售业务内控系统的应用范围，明晰系统范围内各个业务板块中的业务流程以及各业务流程主要环节的风险特征、内控措施和技术;并针对企业内控信息化实施的新特征，准确、有效的提炼出与T环境下内控风险防范紧密相关的实体及其属性，以及相关的函数、、动作序列，建立一个满足销售业务内控需求的信息系统的领域描述模。企业 控制应用指引第9号 销售业务》给出了销售业务应当关注的主要风险以及相应的管控措施，可用表1的形式进行简要概括(限于篇幅，仅简要列示二个流程)。表 稳定忠实的客户群体，级。客户开发不够，客户档案不健全，缺乏合理资信评估，客户选择不不同目标客户确定定价机制和信用方式，客户信用动态管理，权、用、信用等市场开发()、销售管理、会审核确保货物保质保量、货，货品损失或，依据销售合同、订单、等备货出库，制，全程销售登记制销售发货单销售发货管理、仓储管理财从表1的领域分析中，可以抽取出销售业务内控系统的实体:基于不同的抽象层级，对企业内控系统的实体提取方法可以是多样的。从最顶层来看，无论是何种组织框架的企业的内控领域，至少都包含三类实体:隶属于不同角色的职责相关人(r)、企业管理运营相关的各种文档(C)、以及围绕这一系列人员及文档所产生的信息76

流动(MSG实体Actor:内控领域中职责相关人。从不相容职务分离控制来看，一般包括:批准、业务经办、会计记录、财产保管、稽核检查等部门岗位。销售业务不相容岗位至少应当包括:客户管理与信用评估、销售合同的签订与、销售业务经办与审核、办理发货与仓储管理、销售票据管理与销售开票，以及相关会计记录的相互牵制的岗位职责。这些实体可以依照表1中的分析，按照主要岗位和职责、主要业务表单和业务流程中涉及的信息进一步细分。根据不相容的职务如果不实行相互分离的措施，就容易发生舞弊等行为，该实体至少包含人员编号、角色、部门、允许的操作等属性，并可以进一步扩展细化。实体C:领域中的文件。从内控功能的角度来看，可以大致分为三类:(1)系统中的人员、角色、权限、操作限制类文件，这类文件保存了 、职责分离的详信息;(2)业务表单文件，如销售订单、发货单、销售发票，这类文件保存了业务信息，以及业务经办、、稽核等内控制度执行信息;(3)标准文件，如客户信用、销售、各类经费预算等，这类文件保存了预防性控制和发现性控制的数据。该实体至少包含文件编号、处理状态、文件类型、文件内容等属性。实体MG:领域中的信息流动。从内控的角度来看，可以是制度执行流程或某业务流程的控制流程。可以包含信息状态、信息类型等属性。函数:规定领域中实体由输入到输出的变化规则。从内控措施执行流程的角度，该领域的函数主要可以分为信息处理(eDOC)和信息传递(tDOC)两大类。这两类函数的输入输出变化规律定义如下:

收入、成本、应交税金的一系列。动作序列可以用公式表示。二)上述领域分析将原有的基于权力制约和岗位分置的销售业务内控系统转化成以信息流为基础的基于IT 的EFEB描述模型。在此基础上，可利用形式化方法对销售业务内控的领域描述进一步的形式化建模与描述，以便于机器自动验证内控系统性质与领域分析描述性质一致。OTS/CafeOBJ建模主要分为两步: (1)对要分析的对象(领域)建立OTS(状态观测系统);(2)使用CafeOBJ对OTS模型进行描述。建模和证明包含了大量等式描述与证码，限于篇幅，本文仅简要介绍OTS/CafeOBJ的建模对领域分析的EFEB描述建立OTSOTS模型:整个分析对象被看作一个状态观测系统，这个系统有状态空间γ。该状态观测系统S包含系统中对象、该系统的初始状态和状态转换规则，因此OTS模型可表示为三元组:SO，I，T。O:是一个有限集，定义对OTS系统的观测演算子，用来观测OTS某个状态时相应显性数据类型的值。I:是一个有限集，表示OTS系统的初始状态，Iγ。T:Operate

表示在一定条件下状态转换规则的有限集合。领域分析 →MSG'×Δ Actor×Actor×MSG× 其中箭头() 的实体(即输入数据类型)，箭头后表示函数运行后输出的领域中的实体(即输出数据类型)。操作函数(eDOC)表示一个职责人进行某种操作后，实体MG和C都发生了改变。例如，销售开票人员(r)填写一张销售(C)并且签字后(MG)，使得实体C的属性(如:文件内容由空到有具体的数据)和实体MG的属性(如:消息内容由未填写到已填写)发生了改变。传递函数(tDOC)表示输入可以是二个职责人进行某种操作后使得实体MG的属性(内控执行流程)发生了改变而文件C内容没有改变。例如，当销售开票人员开出销售发票并签字传给销售主管，销售主管在上签字后使得MG属性发生了改变而的内容没有改变。: 领域中某个可以触发一连串有联系的函数变换而导致的领域中实体属性变化的具体函数。以一个直接开票的销售业务处理流程为例，当销售经理对上的、产品规格型号、数量、单价等信息审核签字后发出的执行指令，可视为直接开票业务流程的触发器，也可以看作是该业务流程中一个重要。动作序列:领域中一连串有联系且具体的函数变换而导致的领域中实体属性变化的。例如，销售开票执行后，生成相应的发货单、出库单，装运单，以及会计确认

EFEB)OTS三元组的关系如下:OTSO分析中实体的观测;I则是触发一系列状态转换的发 而T描述的是领域分析中的函数，由实体上的函数变换而带来整个系统状态的转换;而S对应的如图3所示，整个销售业务中的所有EFEB看作是一个状态观测系统(OTS)，构建销售业务内控(IC)系统OTS模型，首先要对该模型中所包含的对象actor、doc、msg)、该系统的初始状态(I)(如在销售业务被触发前，公司财务部门已对货物进行了销售定价)、状态转换规则(如客户开发与信用管理等流程中实体的变化规则)进行定义描述，然后使用CafeOBJ进行定理推导和证3OTS使用CafeOBJ对OTS由于CafeOBJ是一种代数方法，它的语义主要是通过CafeOBJ等式来进行表达的。整个内控系统的状态空间γ被描述为CafeOBJ中的隐含数据类型IC。要想得到内控系统中某个实体的状态，则可用一个观测返回CafeOBJ中的可三)在建立了销售业务内控系统的S模型和J描述的基础上，可以用J将模型相应的内控性质的自然语言描述，转换成基于数理逻辑的形式化语言的规范描述，以及通过人机交互系统进行自动的机器推导，以证明所建内控系统模型是否满足内控性质需求。例如，发货控制性质i:如果一个人(actor)在同一个系统中担当互相牵制的角色(role)，将导致发货不符合规定、私自发货、货品损失等风险。该性质的CafeOBJ描述如下:red＜ICi (actori，actorj ＊＜ICj＞suchThat al上述性质通过J定理证明器可直接返回真”值，说明在系统正确使用的情况下，性质i中所描述的风险，是可以通过内控系统实施得到控制和规避的。(四 使用逻辑推理对所设计的销售业务内控系统性质进行证明后，要对不可验证的性质进行分析讨论，修正并完善相关内控制度和控制措施，再应用到企业控制信息化实践中。企业内控信息化实施是社会科学与计算机应用科学深度交叉结合的课题，需要将这二者的设计与实施方法进行有机的结合与运用。从管理软件开发与实施过程来看:内控理念、制度流程、控制措施嵌入信息系统的过程，是将人们用自然语言表达的对企业 控制系统的需求用算机规范的方法和表达工具表达、逐步地转化，最终转化成用计算机程序实现的过程。由于基于T的内控系统既包含了对人、循环、、数据库、信息系统设备等人财物的控制，又包含了利用人、制度、规程、数据库文件、计算机程序等术实施控对这样复杂大统需求，要人们用自然语言表达，不出和缺陷是很难的。 控制规范2010．

京:经济，29～31、56～，．2007．控制执行机制分析框架构建．会计研究，10:46～52罗胜强．2012．企业控制:主要风险点、关键控制点与案例解析．:立信会计，199～224电平，．2004．论环境下会计信息系统的演进．大学学报(人文科学版)，4:437～电平，．2007．企业控制理论的演进及其对国的启示．大学学报(社会科学版)，2:222～228王海林2008IT环境下企业控制模式探讨会计研究，11:63～68．2006．控制理论的困境及其出路．会计研究，2:53～59红，．2011．控制缺陷的识别、认定与报告．会计研究，3:76～802003ISCA模型会计研究，10:30～32，2007．控制工程学研究．会计研究，3:64～70．2007．条件下的控制规范:国际实践与启示．会计研究，7:29～35，．2011．企业控制评价系统研究．审计研究，1:69～78，，高宏伟．2011．以来国内部控制研究及基于2000年到2010年《会计研究》等国内主要七种期的分析．会计研究，11:57～64Bjorner，D．2006．SoftwareEngineering1ionandMg．BjornerD．2006．SoftwareEngineering2SpecificationofSystemsandLanguages．rD．ChenX．，andD．g．2008．ApplicationofDigitalRightsManagementtoAccountingInformationProcessingintheSemanticWebviroet．InternationalConferenceonAdrea，August26～28Futatsugi，K．etal．2005．ProofScoresintheOTS/CafeOBJMd．In:Proceedingofthe6thIFIP6．1InternaFutatsugi，K．，T．Nakagawa，andT．ai．CAFE:An StrengthFormalMd． CreditandCapitalStructureof Wu Inthispaperweexaminehowthecreditaffectthefirms'capitalstructureandtheiradjustmentof846publiclylistedfirmsfrom2001toMleverage，especiallyshorttermleverage．Especially，legalreserverequirementaffectsmostsignificantly，thespreadbetweendepositsandloanscomessecondandcapitaladequacyratioinfluencesslightly．Inaddition，thespeedoffirms'capitalstructureadjustmentishighestanditislowestwhenthespreadbetweendepositsandloansischanged．Withthelegalreserverequirement，thecapitalstructureadjustsmoderay．CurrentSituationofIntangibleAssetsofHigh－techCorporationsinmajordevelopedcountries;focusesonthestructureofintangibleassets，inputandoutputefficiencyoflistedcompaniesinhightechindustrybothfrometangibleassetsisirrationalandR＆Dinvestmentisdeficientwhichshouldbedrawnmoreattention．InternalControlsandtheImmuneSystem:BasedontheThoughtofFunctionysisMethodYangXinglongetal．Metaphorisanimportantmethodinsystem ysis，whichaimstoguideusfromadifferenttoinvestigatethediversityofobjects．"Immunesystem"，asametaphorfortheinternalcontrols，providesausefulreferencetounderstandthebasiccategoriesoftheinternalcontrolsanditsmecha temmakepeoplelthetruth?"，"cantheimmunesystem reasetheeffectivenessofindividuals?"withfunctionysishd．Severalproblemsofempiricalstudiesoninternalcontrolsarealsodiscussedhere．Additionally，weelaboratethepuzzleof"immunesystem"andpointoutthatthefunctionoftheinternalcontrolsshouldstrictlybedistinguished．—AView ysisandFormalprocess，controlmeasurestotheinformationsystemthroughinformationtechnology，andestablishinganintegratedmanagementinformationsystemtomeetinternalcontrolrquns．Itisacomplicatedsystematicproject，soitneedsscientificspecificationmethods，toolsandtechnics． formalmethodsarethemethodsandtechniquesinsoftwareengineering，forhardwareandsoftwaresystem g．abovemethodstotheimplementationofenterpriseinternalcontrolinformatization，canfinddefectseffectivelyandquicklyinthesystemdesignandimplementationintheearlystagebymathematicallogicproving，aswellas，reducetheriskofinefficiencyorfailureofinternalcontrolytes．Thispapertakesasalesprocessasanexampletodiscusstheimplementationofinternalcontrolinformatizationbytheysisandformalhds．CostofResearchUniversityhinaFeng TheconstructionoftheeducationcostinResearchUniversityistheimportantbasisofthefinancialnnt．ThisarticleinviewoftheResearchUniversity