Testing Based on Hybrid System Models

Lee，InsupCCR-0209024许多嵌入式系统是安全关键应用的一部分，例如，航空电子系统、制造业、汽车控制器和医疗设备。 嵌入式应用程序的安全性至关重要的性质，需要更高级别的鲁棒性和可靠性比在传统的软件系统开发的要求。 为了确保设计和实现的更高置信度，目前的实践只是增加了传统验证实践的持续时间、频率、范围等。 最终的结果是开发成本大幅增加，设计周期延长，导致设计周期中的验证瓶颈影响了整体运营有效性、效率和安全性。 该项目旨在通过识别适当的规范形式主义，并使用这些形式主义作为基础，开发全自动化的技术，使用测试来验证实现，以减轻验证瓶颈。 前面列出的嵌入式应用程序的一个重要区别特征是行为的混合（离散和连续）性质。嵌入式系统的连续组件，以及所有工业相关系统的大状态空间，使得基于状态空间穷举探索的验证技术变得棘手。 因此，有必要采用基于抽样的技术来解决验证问题，即，试验. 这需要抽象原始的系统状态空间，以创建一个压缩的状态空间，可以探索到可确定的评估点进行采样。 抽象的方法，选择测试点的方法，以及评估一组测试点相对于另一组测试点的相对价值的方法都是这项工作要解决的问题。本研究还探讨了使用传统的概念，测试覆盖率适用于正式规格的混合系统。 测试套件是使用模型检查器的反例或见证生成技术以及随机路径生成的。通过实现自动化过程所有步骤的工具，解决了演示工作技术的实际问题，以及这些技术应用于实际系统时的有效性：抽象、测试选择、测试推导、测试应用到具体实现，以及测试结果的评估。 工具是在现有的CHARON框架之上开发的，用于创建混合系统模型。案例研究工作基于真实的系统规范，并受益于与霍尼韦尔公司的实践工程师的互动，霍尼韦尔公司是先进航空电子系统开发的领导者。 其中一个问题是如何将这些技术集成到符合DO-178 B航空电子设备认证过程的开发过程中。预计这项工作的更广泛的影响包括：（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.