Testing Based on Hybrid System Models

点击翻译按钮获取中文摘要

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.