Querying Parametric Temporal Logic Properties on Embedded Systems

Most Cyber-Physical Systems are safety critical systems. Some examples of these are aircraft, automobiles, and medical devices. As these systems become more integrated with software, the mistakes and errors within the software can become harder to detect, causing failures that can create expensive damage and ultimately cost human lives. Most Cyber-Physical Systems engineering catastrophes have occurred during transient system behaviors where most system instability occurs. There is a need for a sound verification process in Cyber-Physical Systems design that can provide engineers with the tools to study the robustness of their designs during transient behavior. Researchers at Arizona State University have developed computer software for the creation of Model Based Embedded Systems for Cyber-Physical Systems. The innovation is a Model Based design process that moves most of the work from debugging the prototype implementation of the software to verifying the correctness of the model. This innovation helps designers achieve correct model design by finding errors in the system design more quickly and with greater ease, therefore, reducing project design timeframes. This software tool offers property based exploration and parameter estimation which is not provided by any other product currently available on the market. Potential Applications Health care devices Automotive and air transportation Space exploration Benefits and Advantages Lower Costs Reduces the number of hours required to move a device from initial design to market, so it saves money Faster Reduces the need for physical prototypes, thus reducing project timeframes Reduces Work Load Automatic code generation Download Original PDF For more information about the inventor(s) and their research, please see Dr. Georgios Fainekos' directory webpage