Testing Based on Hybrid System Models

许多嵌入式系统是安全关键型应用的一部分，例如航空电子系统、制造、汽车控制器和医疗设备。嵌入式应用程序的安全关键性质要求比传统软件系统开发要求更高水平的健壮性和可靠性。为了确保设计和实施有更高的可信度，目前的做法只是增加了传统核查做法的持续时间、频率、范围等。最终结果是大大提高开发成本和延长设计周期，导致设计周期出现核查瓶颈，影响整体业务效力、效率和安全。该项目寻求通过识别适当的规范形式化来缓解验证瓶颈，并使用这些形式化作为基础来开发使用测试来验证实现的全自动化技术。前面列出的嵌入式应用程序的一个重要区别特征是行为的混合(离散和连续)性质。嵌入式系统的连续组件，以及所有工业相关系统的大状态空间，使得基于对状态空间的详尽探索的验证技术变得难以处理。因此，有必要用基于抽样的技术，即测试来探讨验证问题。这需要对原始系统状态空间进行抽象，以创建可以探索以确定要采样的可评估点的压缩状态空间。抽象的方法，选择测试点的方法，以及评估一组测试点与另一组测试点的相对优劣的方法，都是本工作要解决的问题。该研究还探索了将传统的测试覆盖率概念应用于混合系统的形式规范。使用模型检查器的反例或见证生成技术以及随机路径生成来生成测试集。演示工作技术的实际问题以及这些技术在应用于现实系统时的有效性，通过实现自动化过程的所有步骤的工具来解决：抽象、测试选择、测试派生、测试应用到具体实现以及测试结果的评估。工具是在现有CHARON框架的基础上开发的，用于创建混合系统模型。案例研究工作基于真实的系统规范，并受益于与霍尼韦尔的实践工程师的互动，霍尼韦尔是先进航空电子系统开发的领先者。一个问题是如何将这些技术集成到符合DO-178B航空电子认证过程的开发过程中。这项工作预计会产生更广泛的影响，包括(1)实践开发人员对正式方法的认识和实际使用的增加，以及(2)安全关键嵌入式系统开发过程的加速，这将使开发周期更短、更安全、更可靠的系统成为可能。

Lee, InsupCCR-0209024Many embedded systems are part of safety-critical applications, e.g.,avionics systems, manufacturing, automotive controllers, and medicaldevices. The safety-critical nature of embedded applications requires a higherlevel of robustness and reliability than is called for in conventionalsoftware systems development. In the attempt to insure a higher level ofconfidence in the design and implementation, current practice merelyincreases the duration, frequency, scope, etc. of traditionalverification practices. The net result is substantially higherdevelopment costs and longer design cycles, leading to a design cyclewhere a verification bottleneck is impacting overall operationaleffectiveness, efficiency and safety. This project seeks to mitigate the verification bottleneck by identifyingappropriate specification formalisms, and using those formalisms as abasis to develop fully automated techniques for verifyingimplementations using testing. An important distinguishing characteristic of the embedded applications listed earlier is the hybrid (discrete and continuous)nature of behaviors. The continuous components of embedded systems, and the large statespaces of all industrially relevant systems, make verificationtechniques based on exhaustive exploration of the state spaceintractable. Therefore, it is necessary to approach the verificationproblem with techniques based on sampling, i.e., testing. This requires abstracting the original system state space tocreate a condensed state space that can be explored to determinevaluable points to sample. Methods of abstraction, methods forselecting test points, and methods for evaluating the relative meritof one set of test points vs. another are all issues addressed by thiswork. The research also explores the use of traditionalnotions of test coverage applied to formal specifications of hybridsystems. Test suites are generated using the counterexample orwitness generation techniques of model checkers as well as random pathgenerations.The practical issues of demonstrating the working techniques, and theefficacy of these techniques when applied to realistic systems, areaddressed through the implementation of tools that automate allsteps of the process: abstraction, test selection, test derivation,test application to concrete implementations, and the evaluation oftest results. Tools are developed on top of the existingCHARON framework for creating hybrid system models.Case-study work based on real system specifications andbenefit from interaction with practicing engineers working for Honeywell, aleader in the development of advanced avionics systems. One issue is howto integrate the techniques into development processes that conform to the DO-178B avionics certification process.Among the broader impacts that are anticipated from this work are (1)an increase in awareness of and actual use of formal methods bypracticing developers, and (2) an acceleration of the safety-criticalembedded system development process that will enable the creation ofsafer, more reliable systems with shorter development cycle times.