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.