Biblio

Modern large scale technical systems often face iterative changes on their behaviours with the requirement of validated quality which is not easy to achieve completely with traditional testing. Regression verification is a powerful tool for the formal correctness analysis of software-driven systems. By proving that a new revision of the software behaves similarly as the original version of the software, some of the trust that the old software and system had earned during the validation processes or operation histories can be inherited to the new revision. This trust inheritance by the formal analysis relies on a number of implicit assumptions which are not self-evident but easy to miss, and may lead to a false sense of safety induced by a misunderstood regression verification processes. This paper aims at pointing out hidden, implicit assumptions of regression verification in the context of cyber-physical systems by making them explicit using practical examples. The explicit trust inheritance analysis would clarify for the engineers to understand the extent of the trust that regression verification provides and consequently facilitate them to utilize this formal technique for the system validation.

Interior permanent magnet (IPM)-type linear oscillating actuators (LOAs) have a higher output power density than typical LOAs. Their mover consists of a permanent magnet (PM) and an iron core, however, this configuration generates significant side forces. The device can malfunction due to eccentricity in the electromagnetic behavior. Thus, here an electromagnetic design was developed to minimize this side force. In addition, dynamic analysis was performed considering the mechanical systems of LOAs. To perform a more accurate analysis, instantaneous inductance was considered according to the mover's position.