Computer systems need to be checked for correctness prior to market launch. However, because of time constraints and the complexity of today's computers, a full verification is often not possible. In the SELFIE project at DFKI's Cyber-Physical Systems department, headed by Prof. Dr. Rolf Drechsler, a fundamentally new approach is being developed that allows systems to self-verify after production and delivery. Researchers are presenting the prototype of a self-verifying system at the Hannover Messe.
Today, embedded and cyber-physical systems are in use in the form of microchips in nearly all areas of everyday life – in smartphones, coffee machines, and electrical toothbrushes as well as in essential safety applications for trains, airplanes, and medical implants. To ensure the correctness of these increasingly complex systems, they are checked for errors during the design phase by various verification procedures. The problem: The growing complexity and ever-shorter product launch cycles force engineers to complete the verification process even though no assurance of full functional correctness can be given at that point. Consequently, errors in the final product often remain undetected.
In Project SELFIE, scientists at DFKI are breaking new ground in how to approach system verification. Equipping devices with additional hardware and software enables them to complete all unfinished verification tasks while in use by the end users. The checks can be accomplished much faster subsequent to delivery since they can be limited to the actual functionality, whereas the verification performed in the design phase must take all possible use scenarios into account. The manufacturer can react quickly if the self-check reveals errors in the system, either with updates, the disabling of certain functionalities, or if necessary in the worst case, a recall.
The method is based on a comprehensive formal design process. Based on the specifications, a model of the system is created that serves as the basis for implementation. In parallel, the characteristics to be verified are prepared in a format that can be detected during operation of the target system. The prerequisite for success in proof of correctness check is having advance knowledge of as many operating parameters as possible. For example, the various sensor controls of a smart home (light, movement, door sensors) and actuators (light, heat, or blinds) can be linked together using certain rules – e.g., "When it gets dark, and a person is in the room, switch on the light. If no one is in the room, the light must remain off." By defining specific use scenarios, checking all possible combinations of sensors and actuators becomes superfluous and the calculation time is much faster. Scientists will demonstrate the new method using a Smart Home System at the Hannover Messe: The user configures the system and then initiates the self-verification. Only if this check returns a successful result, the application is started.