Search Results

Finite State Machines (FSMs) are used at various stages of software development, from the initial concept of software system to the lowest level implementation. These FSMs communicate non-deterministically with the other FSMs and the environment of the underlying system. Any inappropriate handling of the communication across multiple FSMs or environment may lead to unexpected behavior of the underlying system. Manual detection of the root cause of such unexpected behavior is effort intensive. Moreover, state of art techniques focus mainly on design level review of communicating FSMs (Comm-FSMs), and no technique is available for systematic review of Comm-FSMs at implementation level. In this paper we present a review technique for detecting inconsistencies in the implementation of Comm-FSMs.

Verification and Validation (V&V) techniques commonly use static analysis to detect property violations in modern software systems. However, besides checking for general programming errors like division by zero, array index out of bound etc., certain program patterns can also be verified in order to detect inconsistencies in the software. For instance, there could be several strongly related program entities, such as groups of variables or data structure members updated together, which are often observed across various parts of a program. We term such strongly related entities as group variables. When only a subset of group variables is updated at some part of a program, it could probably be a result of some inconsistency in implementation which may lead to unexpected behavior or failure of the underlying system. Therefore, verifying group variables and their write operations is essential to ensure the safety and reliability of software.

A flag is a global boolean variable used to achieve synchronization between various tasks of an embedded system. An application implementing flags performs actions or events based on the value of the flags. If flag variables are not implemented properly, certain synchronization related issues can arise which can lead to unexpected behavior or failure of the underlying system. In this paper, we present an automated verification technique to identify and verify flag usage patterns at an early stage of code development. We propose a two-step approach which consists of: a. identification of all potential flag variables and b. verification of flag usage patterns against predefined set of rules. The results of our experiment demonstrate that the proposed approach reduces the cost and complexity of the flag review process by almost 70%.