DynaMICs软件工程监控：运行时约束验证与可跟踪性

网址：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 17页DynaMICs：全面支持运行时监控A. Q. Gates，S. Roa ch，O. Mondragon和N. 计算机科学德克萨斯大学埃尔帕索分校美国摘要软件工程致力于使软件系统的经济建设，行为可靠，可预测和安全。在其他工程学科中，安全部分是通过对过程的详细监控来保证的。在软件中，我们可以通过监视程序的执行来达到对程序运行的某种程度的信任。DynaMICs是一个软件工具，它有助于收集和使用软件系统的约束。此外，它通过将约束映射到系统工件来支持可跟踪性。约束规范与代码分开存储;约束监控代码从规范自动生成并插入到程序的适当位置;约束在执行时进行验证。这些约束检查由变量值的更改触发。我们描述了DynaMICs的架构，讨论了替代验证技术，并概述了DynaMICs项目的研究方向1引言工程学的梦想是能够构建一个系统，并确信它会按预期运行。在大多数工程领域，这个梦想已经基本实现。然而，在软件领域，它仍然难以捉摸。与其他工程学科不同，软件开发通常需要构建超出开发人员经验范围的系统。此外，集成来自多个领域的知识的必要性增加了当今正在开发的许多系统的复杂性。通过应用诸如能力成熟度之类的过程指南，1 这项工作得到了NASA资助NAG 2 -1012、NAG 2 -1138和NCC 5 -205，Sandia资助BD-9421、CONACYT-68761和NSF资助EIA-9522207和EIA-9729990的支持作者要感谢审查者提出的建设性意见。2 电子邮件：agates，sroach，oscar，ndelgado@cs.utep.educ 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2模型（CMM）、个人软件过程（PSP）和国际标准化组织（ISO）9000.这些指导方针侧重于软件构建的过程。不能保证使用这些方法会产生高质量的软件。例如，不能保证由CMM级别5的组织生产的软件将无故障地执行。存在许多软件验证方法（其中一些在第3节中描述）;然而，缺乏详尽的测试，没有一种方法可以证明复杂系统的代码执行对于所有可能的输入都是正确的化学、工业、电气和土木工程师通过在设计中融入安全功能来构建可靠和安全的系统。例如，锅炉装有减压阀，蒸馏塔装有高温shuto，桥的结构使预测的失效载荷是预测的最大载荷的几倍在仅施工不能确保安全使用的情况与此类似的软件是运行时监控。虽然断言和异常处理已经使用了20多年，但更一般的运行时监视还没有被广泛采用为标准实践，主要是因为性能下降和维护包含检查代码的程序的困难。运行时监控的目标类似于其他保证技术的目标然而，在运行时监控中，我们并不试图证明程序在每种情况下或对所有输入都能正确执行。我们只是试图证明程序的当前执行对于一组指定的属性是正确的。这在某种程度上简化了问题。我们不关心程序可能访问的所有可能的执行路径或状态。我们只关心程序在给定执行中实际访问的那些状态。 在这些状态中的每一个，我们试图证明程序的关键属性被保持。这种方法应该证明是有用的，在检测和隔离故障，并在减少故障和故障之间的差距。通过在运行时监视关键程序属性，应该在错误导致严重故障之前检测到错误。另一个用途是提高在测试期间检测故障的概率。运行时监视的标准方法是一个耗时的过程。通常，程序是相对于规范进行分析的，经常是在试图隔离错误的上下文中进行分析。约束和变量，表明状态的关键元素被识别。代码测试约束或监视变量被插入，然后执行仪表程序。对输出进行分析，并进行校正或重复该过程。这种方法的困难在于它非常耗时，代码的插装可能使维护更加困难，并且通常，为了隔离错误，选择临时的约束和监视事件。3阶段延长工艺驾驶咨询区别特征需求分析和规范从领域专家和用户那里引出并指定约束可以监控哪些行为来检测正确的执行？* 捕获约束并将其与程序分开维护* 自动插入约束* 为约束维护* 通过监视修改代码上的约束来确定更改的影响发展捕获开发人员的假设和限制关于使用软件？测试识别特定于测试的约束在测试过程中需要监控哪些状态信息？维护创建、更新或删除约束有哪些约束条件发生了变化或需要增加？表1DynaMIC提供的扩展和功能在一种称为DynaMIC [13，17，18，19]的方法中，我们通过提供支持约束监控代码的构建和插入并促进对需求故障的跟踪的工具来解决这些问题。DynaMICs的主要特点是，在每个需求，设计和实现级别的约束引起的;约束是从代码单独存储;约束测试代码自动插入到程序在对象代码级;和跟踪机制提供有关违反约束的相关信息。 我们的约束定义的一个显著特征是约束不需要是实现感知的。DynaMIC提供了工具来帮助指定跟踪所需的约束和链接。表1总结了DynaMICs系统所需的软件过程的扩展，给出了驱动约束引出的查询，并总结了这种方法的特征。这项工作是有意义的，因为该方法侧重于识别确保运行时正确行为的约束，并使用这些约束来检测使用其他方法可能难以检测到的错误。如果没有检测到约束冲突，则表示约束得到了保留（至少在代码中测试约束的位置）。跟踪的使用通过维护代码、约束和支持文档之间的关系来促进错误的更正。虽然这种方法不如模型检查或定理证明那么完整，但它通过显示程序在当前执行中相对于4监视的财产。本文的下一节将更详细地描述这种方法。第3节简要讨论了其他核查方法。第4节讨论了项目的未来方向。 本文最后在第5节中进行了总结。2动力学方法DynaMIC与其他方法的区别在于将约束与代码分开，自动生成约束检查代码，自动使用约束检查代码或指令对程序进行插装，并支持在约束、代码和文档之间进行跟踪图1给出了系统的数据流图，其中弧线表示数据流，椭圆表示数据转换，阴影框表示源或接收器，开放式矩形表示数据存储。椭圆上的阴影区分静态完成的那些变换，即，在程序代码执行之前或之后，以及那些动态完成的，即，在程序代码执行期间。约束和知识的定义、监视器的初始化、约束与其支持文档的链接以及约束的静态分析在执行之前完成。监视器的调试包括程序代码的控制流分析、校验码生成和插装。监视和跟踪是动态完成的跟踪也可以在程序执行之后通过使用运行时生成的状态历史来完成每一个主要的转变，即，约束和知识的定义、监视器的初始化、监视以及跟踪和分析将在下面的小节中讨论。2.1约束与知识定义约束捕获领域知识，例如由软件建模的真实世界对象之间的属性、行为和关系，以及实现的假设和限制。与需求获取不同，它会问这样一个问题：“系统将做什么？”约束引出提出了这样一个问题：建模对象的哪些属性指示正确的程序执行？例如，考虑两个整数a和b的除法，得到商q和余数r。对于这个问题，可以定义两个约束：r b和（q b）+ r = a。<约束不会重新计算a和b的除法，而是检查除法是否正确。通常，约束是从需求中收集的。此外，分析师可以通过与领域专家的访谈来识别约束，使用故障树分析[29]等方法来指导问题。约束的其他来源包括用户、客户和开发人员。如图1所示，约束规范存储在约束和知识库中。因为约束可以独立定义，5静态过程动态过程静态动态过程分析师设计师领域专家用户CFG应用对象代码插装目标码查询结果1定义约束和知识初始化监视器监测配置参数质量保证和验证与确认数据字典监测代码状态与约束ID历史日志约 束 / 知 识库迹线和制品储存库分析应用程序源代码追踪查询结果2Fig. 1. 数据 在DynaMICs系统中。在实现的过程中，有必要维护一个数据字典，用于存储规范中使用的变量的类型和描述。约束变量被手动映射到代码变量，并且这个映射被保存在数据字典中。希望自动化约束中使用的变量与代码中使用的变量当约束被指定时，它们被映射到支持文档，例如访谈记录、SRS文档、软件设计文档、备忘录或存储在工件存储库中的通信。其他相关信息（如作者和日期）与约束规范一起维护。约束被指定为事件-条件-动作规则[19]。该事件指示自动化程序检测。条件和动作用于生成约束检查代码。当需要附加信息来计算约束的值时，也必须指定该信息。与约束指定一样，事件指示自动化程序插装。当条件成立时，该操作将导致存储到已在数据字典中声明的特殊变量。例如，在解析输入字符串的程序中，可能需要计算“#"字符的出现次数，以检查对可能包含在字符串.用户需要声明一个维护计数的特殊变量，并指定一个事件，该事件的操作是在“#”字符被读取。 事件、条件和操作如下6代码q = 0;return a;当r>= b{r-= b;q ++}约束控制流图条目B1路径表达式赋值（r，赋值（r，B1 B2 B3 [B4 B3]*B5B2赋值（r，第一条：事件：（{q，r}，intermediate，processing，after-store）条件：a =（q *插装代码q = 0;return a;A：B3第二条：事件：（{r}，delayed，processing，after-store）条件：r b操作：日志当r>= b{r-= b;q ++B：赋值（r，B4B5出}C：活动 事件定义被定义为有序的四元组[16，17]：变量集x转换x阶段x放置，其中变量集：令牌集转换：{立即、中间、延迟}阶段：{输入、处理、输出}放置：{前店，后店}在DynaMIC中，我们将状态定义为约束变量中值的集合。状态转换是某个约束变量的变化。事件的定义包括需要监视什么状态转换以及何时需要监视这些转换的定义。事件定义将约束检查限制到某些执行路径。事件定义的变量集标识了一组要监视的约束变量，这些约束变量必须映射到实现级变量。递减变量用于区分初始、先前和当前状态。图二.除法示例的约束检测。“过渡”、“阶段”和“放置”描述何时应进行约束检查阶段用于限制约束的测试。例如，当Phase为Input时，当通过输入操作更新变量时，将测试约束。如果阶段为“正在处理”，则在对变量进行赋值时测试约束。如果Phase为Output，则在输出系统调用中使用变量时测试约束。因为计算值可能不存储到存储器，而是经由输出指令存储到设备，所以还需要将输出指令视为引起状态转换的指令。对于指定的相位和变量集，中间转换指示约束必须在每个状态转换之后保持。 Delayed表示约束必须在一个speci结束时保持，ed阶段。例如，指定的变量a、b和c的约束7分别作为Transition和Phase的Delayed和Input，表示在读取了这些变量的所有值之后执行相关的监控代码。如果程序使用迭代构造读入这些值，则检查将发生在迭代构造终止的点。在嵌套迭代构造的情况下，检查将发生在最外面的构造之外。中间转换指定在某个状态转换序列之后约束必须保持图2提供了一个使用划分示例在第2.1节中。在图中，请注意，每次将值存储到r和q时都会检查约束C1（中间和处理）（请参见图2中的标签A：C1和B：C1）。在所有存储到r之后检查约束C2，即，while循环终止时（参见图2中的标签C：C2我们假设敏感设备的控制是内存映射的，因此使用赋值访问[19]。放置指示约束是在违反将导致灾难性故障的约束（称为关键任务约束）的情况下，必须在存储值之前检查约束。对于非关键任务的约束，测试可能发生在写入变量之后，因此可以并行检查以减少对性能的影响。条件条件定义用一阶语言表示[12]。除了指定程序变量之间的关系之外，条件还可以确定以下是否成立：与程序变量相关联的值在值的范围内或者是值集合的成员一个程序变量在使用前已经被赋值，两组值是不相交的（例如， 兼职员工不被归类为全职员工），或者一个集合是另一个集合的子集（例如，所有奖学金获得者均登记为全日制学生）。行动上动 作 定义指定违反约束的后果。这可以包括诸如在历史日志中记录状态、保存状态以进行错误恢复、执行状态回滚或启动优雅降级等操作。 后三项行动目前正在研究之中。见图3对于示例约束。 在这个约束中，变量Nkpower被mon-n-伊托。放置值Before-store表示在将值存储到Nkpower之前立即检查约束。条件中给出的约束规定，如果On（Nkpower）在拦截的更新中保持，则Stable（X）必须保持。2.2监控和执行程序代码可以通过使用内联指令序列、函数调用或在单独进程上启动约束检查的触发器来使用约束检查代码进行仪表化[9]。 如前所述，规范的事件定义以及程序执行过程的分析8约束：事件：条件：措施：系统应确保在命令NK电源之前X必须稳定。（{Nkpower}，Immediate，Processing，Before-store}开启（Nkpower）->稳定（X）日志图三. 示例规范。指导程序执行中应执行约束检查的点[14]。DynaMIC遵循的分析方法侧重于路径表达式[1，25，41]，即，从执行控制流图（CFG）导出的正则表达式，其中每个节点都是一个基本块，用读/写列表进行了注释（参见图2）。这些表达式进行了分析，以确定- tify程序插装点。插装点很重要，因为它们标识代码中修改约束中使用的感兴趣变量（VOI）的位置在[17]中可以找到一个定义约束的仪器点的通用算法。该算法没有考虑所有类型的中间约束. 该算法的扩展正在研究中。图2说明了第二节中给出的除法示例的仪表化过程第2.1条。分析可以在源代码、中间代码或目标代码级别进行。在内存映射I/O系统中，可能需要在测试约束之前防止写入内存。由于安全关键系统需要保证，而不是由当前的编译器提供，关键任务约束的检查需要在对象代码级的仪器。监视器的角色被委托给执行应用程序代码的进程，或者委托给不一定在同一进程上的另一个进程。当使用单独的进程时，必须传递足够的状态信息来验证约束，对于关键任务约束，进程之间的同步是必要的[42]。监视器观察正在执行的程序，当它检测到违反约束时，它执行与约束相关联动作可以是记录状态，通知DynaMIC的跟踪和分析组件2.3追踪与分析跟踪[7]是在开发过程中跟踪工件之间的链接以识别和记录工件的起源和分解的活动。例如，需求规范文档中的需求可以链接到软件源代码中的方法。跟踪提供了证明软件系统开发过程中使用的工件的完整性、必要性和一致性的能力，并且工件包含或实现了前一个工件的所有需求。9开发人员[客户、用户、领域专家]动态创建定义约束连杆创建连杆至链接到链接到手动创建连杆至SRS设计文档文档测试文档…代码伪影见图4。 高级FasTLInC可追溯性模型。与传统的可追溯性模型不同，Dy-naMIC [15]中使用的跟踪方法称为基于约束的跟踪，侧重于约束。跟踪由DynaMIC的一个组件执行，称为使 用 完 整 性 约 束 的 快 速 跟 踪 （ FastTracing with Links using IntegrityConstraints，FasTLInC）。FasTLInC子系统建立约束和工件之间的关系，并促进违规分析。使用约束来自动定义代码链接和捕获运行时信息是基于约束的跟踪方法与其他方法的区别。FasTLInC通过遍历从应用程序代码到约束以及从约束到工件的路径进行跟踪。图4给出了基于约束的可跟踪性模型的高级视图。 虽然FasTLInC不像传统的跟踪方法那样支持工件之间的跟踪，但它可以与现有的工具（如TOOR [33]或SODOS[23]）集成以提供此功能。由于DynaMIC可验证程序是否符合约束条件，因此FasTLInC提供的可追溯性非常重要，因为监控器的目标是检测由需求中的模糊性和变化、需求之间的冲突以及程序使用的变化引起的故障。自动识别约束和代码之间的双向链接消除了管理链接的繁重任务，由于代码的进化性质，这可能是有问题的。此外，该方法还支持约束管理、变更管理、错误源识别以及约束和工件之间冲突的解决。FasTLInC用作约束、知识和数据字典条目的数据库管理系统约束可以被分组在一起以形成工作集，即，分组10约束规范，它们共享共同的属性，如日期、作者、变量名或事件分类的方面。通过查看工作集，开发人员可以检查约束，以检查它们之间的不一致性，并检查从多个来源收集的知识，并在生命周期的早期纠正可能的差异[13]。FasTLInC与工件和历史日志存储库以及监控代码交互。 FasTLInC通过提供对系统管理的数据的访问，协助跟踪并支持违规行为的协调。历史日志允许用户在检测到违规时或在程序完成执行后跟踪和研究程序行为。在DynaMIC中，任何约束及其相关工件都可以链接到约束检查或知识计算发生的程序执行点。相反，FasTLInC提供了在示波器上搜索的功能，即，检索检查指定代码段的约束3相关工作我们将可用于提供正确程序执行证据的技术分为两大类：在部署软件产品之前应用的技术和在部署产品之后应用的技术。预部署技术包括在交付和安装软件系统之前使用的活动部署后技术是与软件系统一起打包和安装的技术，在执行期间用于评估执行的成功和进度。在下面的小节中将讨论这些类别中的每一个，重点是自动化技术。3.1部署前技术预部署技术包括静态应用的技术（例如，程序合成、正确性证明、代码分析和检查）以及动态应用的那些（例如，测试和模型检查）。程序合成。诸如演绎合成和转换合成的方法通过构造可证明正确的软件来解决正确性问题[10，32]。虽然这些系统产生高质量和高保证的软件，但它们是昂贵的。目前使用的许多技术和工具都依赖于软件行为的形式化规范和特定领域知识的形式化规范。一般来说，收集和具体说明这些知识是困难的。这是可能的，甚至很可能，错误将在规范。最后，如果工具依赖于涉及搜索的自动推理，则搜索空间往往是指数的。因此，这些方法不能很好地扩展。正确性证明。对于正确性证明，困难在于构造证明。与程序合成一样，有必要将11大量的领域和编程知识，以便构造证明[6]。随着程序规模的增加，证明的复杂性也会增加。自动定理证明器具有指数搜索空间，使用这种方法的工具不能很好地扩展。在实践中，只有关键的、容易出错的代码区域才能使用这种技术证明是正确的。代码分析和审查。代码评审包括代码检查和巡检。这些都是手工的、人力密集型的活动。研究表明，这些可以导致代码中错误的数量减少十倍[11]。代码可以被注释以增强检查[44]，或促进验证条件的自动推导[2]。试验. 测试是验证系统最常用的技术。测试的困难在于进行详尽测试以保证正确性的不可行性以及与广泛测试相关的成本模型检查。模型检测[6，22，36]是一种用于证明模型满足给定属性的技术。 它能够正确构建复杂的系统，并在各种应用程序中暴露错误方面非常成功。 模型检查器通常有两个困难：创建一个精确的模型，以及必须探索的状态空间的爆炸。系统模型可以用nite状态转换图表示状态爆炸问题的出现是因为被验证的模型中的状态数量是系统的并行组件数量的指数[4]。3.2展开后技术部署后验证技术包括多版本编程和运行时监控。每一个都在下面讨论。多版本编程。多版本编程涉及编写多个版本的软件，并允许软件在运行期间对结果进行投票。在这种方法中，独立的团队为单个规范实现解决方案。假设团队将开发不同的算法，并且多个团队在单个函数的计算中引入错误的概率很小。不幸的是，共享规范可能导致常见故障。此外，个人往往在问题的更困难的部分犯错误，而不是随机的。运行时监控。通过运行时监视，程序在执行时被检查，以确保其行为与预期的行为相匹配。通常，这是通过根据与执行状态相关联的断言来定义预期行为来实现的。有许多方法可以实现运行时监控[3，5，24，27，30，35，38，40]。这些可以被分类为硬件、软件和混合[39]。混合监控，如[20]，将硬件和软件监控结合在一起。硬件监控，如[42，43]，需要使用专门的硬件平台，12应用程序运行。在这种设置下，观察者硬件在程序执行时监视程序。这种类型的监视不会侵入程序代码;但是，数据是在低抽象级别捕获的，因此很难解释。与硬件监控类似的软件是创建一个观察者进程，在程序执行时对其进行监控。这里，执行程序在执行时向观察者进程发送状态信息，观察者进程分析状态信息。这方面的一个例子是[21，45]。类似的方法[27，28，26]是使用将状态信息与高级事件相关联的事件规范。在这种方法中，观察者将需要检查的信息传递给运行时监视器。观察者架构的优点是对原始程序的更改最小化，减少了对程序执行的影响。缺点是程序必须将足够的状态信息传输给观测器，以便运行约束检查，并且在违反约束的情况下，观测器更难停止程序执行软件监控的另一种方法是在程序中插入测试断言的代码。 断言在程序执行时进行测试。一种常见的方法[30，35，38]是开发人员在开发程序时手动创建并在程序源代码中插入约束测试代码。这个过程可以通过用断言注释程序源代码并在编译时注释时生成断言测试来部分自动化。自动确定用于约束检查的插入点的方法包括[17，27]。更传统的软件监控方法需要从执行程序开始循环来分析状态信息。运行时监视的一个简单扩展是事后分析。事后分析[15，21]类似于运行时监控，检查程序特定执行的状态序列。此外，当程序执行时，存储关于程序访问的状态的信息。状态信息的序列称为执行跟踪。程序完成后，分析执行跟踪。优点是程序不需要在运行时测试约束;因此，性能降级被最小化，并且一些时间约束（例如，属性P保持直到属性Q变为真）可以在执行跟踪中的任何状态处被验证。缺点是不能防止故障的发生。4研究方向DynaMICs系统还不成熟，但是，根据我们的实验，我们认为它显示出作为现有验证方法的扩展的前景。它的一部分已经原型化，并已在玩具问题上得到演示我们的目的是改进这个系统，并将其应用于现实世界的软件开发。13[16，34]。为此，我们确定了今后工作的领域。本节概述了最重要的研究和发展：应用时序逻辑，插入约束监控代码的一般程序，与监控相关的性能问题，以及算法的可靠性。时态逻辑的应用。 一些实践者可能会发现，在正式的时态逻辑中表达约束是令人生畏的。 我们的规范语言是更直观的，我们的目标是表明，我们的约束可以表示在一个时间逻辑，因此，它可能是利用推理系统，利用时间逻辑的优势。 使用[8]中定义的语言，DynaMIC规范中的事件E和条件C可以表示为：2（Es ！sC），其中Es 表示在状态s中发生的事件，sC表示条件C在紧接着s之后的状态中成立，并且2P表示P在当前和所有未来状态中成立。在DynaMIC中，自动推理对于识别不一致性至关重要，这是该方法解决的主要软件开发问题之一。性能运行时约束监视的一个主要缺点是性能下降。为解决这一问题，正在研究两种办法。一个是识别可以静态证明的约束，减少需要动态检查的约束数量。第二种方法是将约束监控中的至少一些加载到协处理器。该协处理器将使用snoopy协议来观察存储器访问的序列，并在对感兴趣的变量进行存储时触发约束监控主处理器和协处理器之间的同步是必要的，特别是在任务关键性约束的情况下。插入约束监控代码。 到目前为止，我们能够插入的约束监视代码与感兴趣的变量中的更改事件相关联 我们还没有解决间接、过程调用参数、动态绑定或仅存储在寄存器中的中间值（当检查目标代码时）的问题。单独的静态分析可能不足以在执行期间确定适当的监视点窥探/协处理器方法对于捕获对存储器的间接访问可能是有价值的，因为协处理器将基于对存储器的访问来触发约束测试，无论是通过直接引用还是间接引用进行的。看来，有一些有用的约束条件需要对使用和分配进行监控。例如，考虑前提条件，“忽略漂移压力传感器的输出”[31]。有两种不同的用途传感器的输出值。其中一个用于计算压力。另一个用于确定传感器是否漂移。 前者在传感器漂移时不允许，而后者在任何时候都允许。我们尚未考虑监测感兴趣的变量的使用。健全。 有两个关于健全的 关 注 ，14监视器.一个是只要存在违规，监视器就会检测到违规，另一个是不检查约束，因为它们可能导致错误的检测。换句话说，我们希望确保监视器不会产生假阴性或假阳性。5总结下面的陈述总结了程序验证的艺术状态：“我们不能告诉你它有多好，但我们可以告诉你我们有多努力”[37]。虽然已经成功地证明正确性使用形式化的方法，方法，如定理证明和演绎合成，SIS是不能提供保证，执行代码的复杂系统是正确的所有可能的输入。因此，希望向程序添加安全特征，以便确定程序是否如预期那样运行。与使用定理证明进行程序验证一样，DynaM- ICs方法显示了正确性.然而，我们不是证明有效性，而是证明断言对于模型的特定解释的满意能力，即，当前程序执行的解释。我们认为，这是最重要的解释。DynaMICs方法与其他监控方法的不同之处在于，在软件开发生命周期的所有阶段都会引出约束，并且程序代码的插装是自动化的。我们相信，该方法提供的自动化，监视程序正确行为的能力，以及跟踪工件的能力将激励约束的捕获和使用支持约束推理和需求中潜在不一致性检测的工具将使该方法更具吸引力。引用[1] Bertolino，A.，和M. Marr e，递归地导出路径表达式，Proceedings IEEESecond Workshop on Program Comprehension，177{185}，1993。[2] Bonnier，S.，和T. Heyer，COMPASS：A Comprehensible Assertion Method，TAPSOFT '07 ： Theory and Practice of Software Development ， LectureNotes in Computer Science，803{817，1997.[3] Bruegge， B.， T. Gottschal和B. Luo， A Framework for Dynamic ProgramAnalyzers ， Proceedings of the Eighth Annual Conference on Object-Oriented Programming Systems，Languages，and Applications，65{82}，1993.[4] Campos，S.，和E. 张文，“基于量化符号算法的实时系统分析与验证”，北京科技大学出版社，1999。15[5] Chodrow，S.，和M. Gouda，Sentry系统的实现，软件实践和经验， 25（1995），373{387。[6] Clarke，E. M.的情况，J. M. Wing等人，形式化方法：最新技术和未来方向，ACM计算调查，28（1996），626{643。[7] DoD-Std-2167A。\MilitaryStandard：DefenseSystemSoftwareDevelopment，”国防部，华盛顿特区，1988.[8] Dardenne，A.，A. van Lamsweerde和S. Fickas，Goal-directed RequirementsAcquisition，Science of Computer Programming，20（1993），3{50.[9] 费尔南德斯，F.、机器人驱动方法到Monitoring IntegrityConstraints， ”Master's Thesis， The University of Texas at El Paso， ElPaso，Texas，1998.[10] Flener ， P. ， 《 从 不 完 全 信 息 综 合 逻 辑 程 序 》 ， Klewer AcademicPublishers，Norwell，MA，1995。[11] Freedman，D. P.，和G. M. Weinberg，\手册的步行，检查和技术审查，评估程序，项目和产品，”多塞特宫，纽约，纽约，1990年。[12] Gates，A.，关于定义一类完整性约束，第八届软件工程和知识工程国际会议论文集，338{344，1996。[13] Gates，A.，和S.李，软件故障及其通过DynaMIC的检测，IASTED软件工程会议论文集，323{327}，1998。[14] Gates，A.问：O.蒙德拉贡岛Roach和A. Provetti，\Object-level ConstraintInstrumentation：From Control Flowgraphs to Path Expressions，技术报告，2001年。[15] Gates，A.问：和O. Mondragon，基于约束的跟踪方法，将出现在系统与软件杂志，2002年。[16] Gates，A.问：和S.陈晓，知识管理与自动化约束监控的框架，2001年蒙特雷研讨会论文集：软件密集型系统集成的工程自动化，154-168，2001年。[17] Gates ， A. 问 ： 和 P.J. Teller ， DynaMICs ： An Automated and IndependentSoftware-Fault Detection Approach，Proceedings of the Fourth InternationalHigh-Assurance Systems Engineering Symposium，1999年11月19日[18] Gates，A.问：和P.J. Teller， An Integrated Design of a Dynamic Software-Fault Monitoring System，Journal of Integrated Design Process Science，14（2000），63{78.[19] Gates，A.问：和P.J.Teller，《具有完整性约束的动态软件监控：软件开发和演化的统一方法》，技术报告，2001年。16[20] Haban，D.，和D. Wybranietz，分布式系统行为和性能分析的混合监视器，IEEE软件工程学报，16（1990），197{211。[21] Havelund，K.，使用Java分析指导Java程序的模型检查，第七届国际SPIN研讨会，斯坦福大学，加利福尼亚州，2000年。[22] Holtzmann ， G. ， SpinModel ， IEEETransactionsonSoftwareEngineering，23（1997），279{295.[23] Horowitz，E.，和R.陈文辉，《软件工程》，北京：软件工程出版社，2000年。[24] Je ery，C.，W. Zhou，K. Templer和M.刘晓波，一种用于程序执行监控的轻量级体系结构，软件工具和工程的程序分析ACM SIGPLAN/SIGSOFT研讨会，67{74}，1998年。[25] Kidd，M.，在路径表达式的启发下确保基于计算机的系统中的高后果关键事件序列，基于计算机的系统工程国际会议和研讨会论文集，483{ 490}，1997年。[26] 金，M.，M. 你看， \MaC：实时系统的实时正确性保证框架，”技术报告，1998年。[27] 金，M.，M. Viswanathan等人，时间属性的正式指定监控，欧洲实时系统会议论文集，1999年。[28] 李岛，加-地H. Ben-Abdallah等人，运行时正确性保证，1998年韩美会议录1998年战略技术会议。[29] Leveson，N. G.，\Safeware：System Safety and Computers，”Addition-Wesley，Reading，MA，1995.[30] Luckham，D.，W. Mann，S. Meldal和D. Helmbold， An Overview ofAnna：Speci cation Language for Ada，IEEE Software，20（1988），9{23.[31] 卢茨河R.，和H.Shaw，\DS-1试验性断言实现：经验总结，”技术报告，喷气推进实验室，帕萨迪纳，CA，1997年。[32] Manna ， Z. ， 和 R. J. Waldinger ， A Deductive Approach to ProgramSynthesis，ACM Transactions on Programming Languages and Systems，2（1980），90{121}。[33] Pinheiro ， F. ， A. 郭 文 贵 ， 一 种 面 向 对 象 的 需 求 跟 踪 工 具 ， IEEESoftware，13（1996），52{64}。[34] Roach，S.，和A. Q.陈志华，自动化程式分析、测试与验证，国立成功大学硕士论文，2001年。17[35] Rosenblum ， D.S. ， A Practical Approach to Programming with Assertions ，IEEE Transactions on Software Engineering，21（1995），19{31.[36] Rushby，J.，并行过程的建模与验证中的验证定理证明”（F.Cassez编），Springer-Verlag，Nantes，France，2000.[37] Rushby，J.，2000年11月在新墨西哥州[38] Sankar，S.和M. 陈文，“程序设计与实现”，清华大学出版社，1993年。[39] 施罗德湾一、联机监测：一种计算机，IEEE计算机，28（1995），72-78。[40] 索西奇河 Dynascope：A Tool for Program Directing，Proceedings of the 5thACMSIGPLANConferenceonProgrammingLanguageDesignandImplementation，12{21}，1992.[41] 塔 尔 扬 河 E 、 路 径 问 题 求 解 的 快 速 算 法， ACM 杂 志 ， 28 （ 1981 ） ，584{614。[42] Teller ， P. ， M. Maxwell 和 A. Gates ， Towards the Design of a SnoopyCoprocessor forDynamicSoftware-FaultDetection ， Proceedings of the18thIEEE International Performance ， Computing ， and CommunicationsConference，310{317}，1999.[43] 蔡，J.P.，K. Fang，H. Chen和Y.李文，一种基于非干扰的实时软件测试与回放机制，《软件工程学报》，1990年，第16期，[44] van Emden，M. H、代码的结构化检查，软件测试，验证和可靠性，2（1992），133{153。[45] Visser，W.，K. Havelund等人，Java Pathfrom-Second Generation of a JavaModelFrom-CAV Workshop on Advances in Veri cation，2000年7月