Verification Tool Support for CRSM

Background:
Many of the safety-critical embedded applications are distributed in nature. Recently a new paradigm, called Communicating Reactive Processes, has been proposed. Communicating Reactive State Machines (CRSM), is based upon this paradigm and extends languages like Statecharts and Argos for distributed applications.

Aim:
The broad aim of this project was to provide tool support for efficient and automatic verification of CRSM programs. Given a CRSM program and a property, the tool should verify whether the property is satisfied by the program and if not, provide the sequence of states that violate the property.

Approach:
STeP is chosen for verification. The main component of the proposed tool is the translator that converts CRSM programs into SPL. The properties are expressed in linear temporal logic.

Outcome:
A prototype implementation of the tool is complete now. The tool accepts tCRSM, a textual version of CRSM. The desired properties are expressed in the language of linear temporal logic involving signals and state symbols in the input CRSM program. The tool works fine for small CRSM programs.