Advances in Computers by Atif M. Memon

Author:Atif M. Memon
Language: eng
Format: epub
ISBN: 9780128151204
Publisher: Elsevier Ltd.
Published: 2018-02-14T16:00:00+00:00

3.2 Analysis and Verification of Statechart-Like Models

Model checking-based approaches: The majority of existing analysis methods for Statechart-like models (e.g., UML state machines, UML-RT, STATEMATE, and Stateflow) require a translation to the input language of existing formal verification tools, mainly model checkers such as SPIN [41] or SMV [42]. Most of the time, the translation process is nontrivial and it restricts the support of the key features of the model to those supported by the model checker to be used and hence makes integration and use with modern MDE tools difficult. Another category of approaches analyze the C or Java code generated from these models and use one of the model checkers for these languages (e.g., Java Pathfinder [43] or CBMC—a Bounded Model Checker for C and C++ [44]). On the other hand, there are fewer approaches that intend to provide domain-specific analysis capabilities by developing domain-specific model checkers that are tailored to the modeling language of interest and hence support more sophisticated features and reduce the semantic gap between the modeling language and the specification language of a general-purpose model checker (e.g., the verification methods implemented within the FUJABA Real-Time tool [45] or the VIS model checker in a very early version of the Rhapsody tool [46]).

Symbolic execution-based approaches: Besides the model checking-based approaches, there are several approaches that adopt the symbolic execution analysis technique of programs and use it in the context of state-based models including:

• Modechart specifications (a variation of Harel Statecharts that incorporates timing constraints in the models) for test sequences generation [47];

• Labeled Transition Systems (LTSs) for test case generation [48] and test case selection [49];

• Input Output Symbolic Transition Systems (IOSTSs) [2] for test purpose definition;

• STATEMATE Statecharts [17] and UML State Machines [18] for verifying temporal properties of the subject models;

• Simulink/Stateflows [50] for analysis and test case generation of flight software using Java PathFinder and Symbolic PathFinder;

• UML-RT State Machines [3] to support a variety of analyses for this type of models.

Download

Copyright Disclaimer:
This site does not store any files on its server. We only index and link to content provided by other sites. Please contact the content providers to delete copyright contents if any and email us, we'll remove relevant links or contents immediately.