ptolemy.verification.kernel
Class REDUtility

java.lang.Object
  ptolemy.verification.kernel.REDUtility

public class REDUtility
extends java.lang.Object

This is an utility for Ptolemy model conversion. It performs a systematic traversal of the system and convert the Ptolemy model into communicating timed automata (CTA) with the format acceptable by model checker RED (Regional Encoding Diagram Verification Engine, v.7.0).

The conversion mechanism roughly is based on the technical report UCB/EECS-2008-41 with some modifications. Basically, the token would not be accumulated in the port of the FSMActor - therefore buffer overflow property would no longer exist in this implementation; it would only happen in the TimedDelay or NondeterministicTimedDelay actor.

For a successful conversion, we simply disallow a system to have super dense time tag with the format (\tau, i), where i>0. In our context this only happens when there is a TimedDelay actor with its parameter equals to zero. For systems with super dense time tag with the format (\tau, i), where i>0, the system can still be converted. However, please note that the semantics might no longer be preserved.

One important feature in our converted model is the use of "complementary" edges. This is used to handle the situation where the FSMActor must react to an arrival of token in the incoming port, but the token can not trigger any transition. For this case, the 'present' token should turn to be 'absent' as time advances. To avoid including any unnecessary behavior we add one "invalid" transition, mentioning that the FSMActor will perform a "stable" move, and at the same time the token will be bring to absent state.

For the tool RED, all time constants should be an integer. This is not a problem because the unit is actually not specified by the timed automata. Therefore, we expect users to use integer values to specify their delay or period.

Limitations: Simply following the statement in the technical report, we restate limitations of the conversion. The designer must understand the boundary of variable domain for the model under conversion. Also, due to the use of complementary edges, complex guard conditions are currently not supported.

Since:

Ptolemy II 8.0

Version:

$Id: REDUtility.java 59167 2010-09-21 17:08:02Z cxh $

Author:

Chih-Hong Cheng, Contributor: Edward A. Lee

Accepted Rating:

Red (patrickj)

Proposed Rating:

Red (patrickj)

Nested Class Summary

private static class	REDUtility.REDModuleNameInitialBean
private static class	REDUtility.REDSingleEntityBean
private static class	REDUtility.REDTransitionBean
private static class	REDUtility.VariableInfo

Field Summary

private static java.util.HashMap<java.lang.String,REDUtility.VariableInfo>

_variableInfo

Constructor Summary

REDUtility()

Method Summary

private static java.util.HashSet<java.lang.String>	_decideGuardSignalVariableSet(FSMActor actor) This private function is used by the private function _translateFSMActor to generate the set of signals used in the guard expression.
private static java.util.HashSet<java.lang.String>	_decideSynchronizerVariableSet(Entity entity) This private function is used to decide the set of global synchronizers used in the entity.
private static java.util.HashSet<java.lang.String>	_decideVariableSet(FSMActor actor, int numSpan) This private function decides inner variables used in the actor.
private static java.util.HashSet<State>	_enumerateStateSet(FSMActor actor) Perform an enumeration of the state in this actor and return the name of the states.
private static java.util.ArrayList<java.lang.String>	_enumerateString(int index, java.util.ArrayList<java.lang.String> paraEnumerateString) This private function generates all possible combinations of string with length i with character 0 and 1.
private static java.util.ArrayList<REDUtility.REDTransitionBean>	_generateTransition(FSMActor actor, State state, java.util.HashSet<java.lang.String> variableSet, java.util.HashSet<java.lang.String> globalSynchronizerSet) This private function is used to generate the transition description for a certain state in a certain actor.
private static java.util.HashMap<java.lang.String,java.lang.String>	_retrieveVariableInitialValue(FSMActor actor, java.util.HashSet<java.lang.String> variableSet) A private function for generating initial values for the initial variable set.
private static FSMActor	_rewriteModalModelWithStateRefinementToFSMActor(ModalModel modalmodel) This is an experimental function which analyzes a ModalModel and flatten it into a single FSMActor.
private static REDUtility.REDSingleEntityBean	_translateBBNondeterministicDelayedActor(BoundedBufferNondeterministicDelay delayedActor, java.lang.String inputSignalName, java.lang.String outputSignalName) Translate a bounded buffer, nondeterministic delayed actor.
private static REDUtility.REDSingleEntityBean	_translateBBTimedDelayedActor(BoundedBufferTimedDelay delayedActor, java.lang.String inputSignalName, java.lang.String outputSignalName) This is an utility function which performs the translation of a single TimedDelay actor into the format of communicating timed automata (CTA) acceptable by model checker RED.
private static REDUtility.REDSingleEntityBean	_translateClockActor(Clock clockActor, java.lang.String outputSignalName) This is an utility function which performs the translation of a single clock actor into the format of communicating timed automata (CTA) acceptable by model checker RED.
private static REDUtility.REDSingleEntityBean	_translateFSMActor(FSMActor actor, int span, java.util.HashSet<java.lang.String> globalSynchronizerSet) Translate an FSM actor.
private static REDUtility.REDSingleEntityBean	_translateTimedDelayedActor(TimedDelay delayedActor, java.lang.String inputSignalName, java.lang.String outputSignalName, int bufferSize) This is an utility function which performs the translation of a single TimedDelay actor into the format of communicating timed automata (CTA) acceptable by model checker RED.
static CompositeActor	generateEquivalentSystemWithoutHierarchy(CompositeActor originalCompositeActor) This function generates an equivalent system which is flattened.
static java.lang.StringBuffer	generateREDDescription(CompositeActor PreModel, java.lang.String pattern, MathematicalModelConverter.FormulaType choice, int span, int bufferSizeDelayActor) This is the main function which generates the system description which is acceptable by the tool RED (Regional Encoding Diagram).
static boolean	isValidModelForVerification(CompositeActor model) This function decides if the director of the current actor is DE.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

_variableInfo

private static java.util.HashMap<java.lang.String,REDUtility.VariableInfo> _variableInfo

Constructor Detail

REDUtility

public REDUtility()

Method Detail

generateEquivalentSystemWithoutHierarchy

public static CompositeActor generateEquivalentSystemWithoutHierarchy(CompositeActor originalCompositeActor)
                                                               throws NameDuplicationException,
                                                                      IllegalActionException,
                                                                      java.lang.CloneNotSupportedException

This function generates an equivalent system which is flattened. It would perform a rewriting of each ModalModel with hierarchy to an FSMActor. Note that in our current implementation the rewriting only supports 'state refinements'.

Parameters:

originalCompositeActor - original system under processing

Returns:

a flattened equivalent system.

Throws:

NameDuplicationException

IllegalActionException

java.lang.CloneNotSupportedException

generateREDDescription

public static java.lang.StringBuffer generateREDDescription(CompositeActor PreModel,
                                                            java.lang.String pattern,
                                                            MathematicalModelConverter.FormulaType choice,
                                                            int span,
                                                            int bufferSizeDelayActor)
                                                     throws IllegalActionException,
                                                            NameDuplicationException,
                                                            java.lang.CloneNotSupportedException

This is the main function which generates the system description which is acceptable by the tool RED (Regional Encoding Diagram).

For hierarchical conversion, here we are able to deal with cases where state refinement exists. For a modalmodel with state refinement, we first rewrite it into an equivalent FSMActor.

Parameters:

PreModel - The original model in Ptolemy II

pattern - The temporal formula in TCTL

choice - Specify the type of formula: buffer overflow detection or general TCTL formula

span - The size of the span used for domain analysis.

bufferSizeDelayActor - The buffer size of the TimedDelay actor.

Returns:

A Communicating Timed Automata system description of the original system

Throws:

IllegalActionException

NameDuplicationException

java.lang.CloneNotSupportedException

isValidModelForVerification

public static boolean isValidModelForVerification(CompositeActor model)

This function decides if the director of the current actor is DE. If not, return false. This is because our current conversion to CTA is only valid when the director is DE.

Parameters:

model - Model used for testing.

Returns:

boolean value indicating if the director is DE.

_decideGuardSignalVariableSet

private static java.util.HashSet<java.lang.String> _decideGuardSignalVariableSet(FSMActor actor)
                                                                          throws IllegalActionException

This private function is used by the private function _translateFSMActor to generate the set of signals used in the guard expression. Each of the signal used by the guard expression would need to have a process representing the port receiving the signal.

Parameters:

actor - The actor under analysis.

Returns:

Set of signals used in guard expressions in the FSMActor.

Throws:

IllegalActionException

_decideSynchronizerVariableSet

private static java.util.HashSet<java.lang.String> _decideSynchronizerVariableSet(Entity entity)
                                                                           throws IllegalActionException

This private function is used to decide the set of global synchronizers used in the entity. When we later return the set, the system would use another set container to store the synchronizer to make sure that no duplication exists.

Parameters:

entity - entity under analysis

Returns:

The set of synchronizers used in this entity

Throws:

IllegalActionException - If thrown while getting the initial state of the actor.

_decideVariableSet

private static java.util.HashSet<java.lang.String> _decideVariableSet(FSMActor actor,
                                                                      int numSpan)
                                                               throws IllegalActionException

This private function decides inner variables used in the actor. It later perform a systematic scan to generate the initial rough domain, and use a constant span to expand it.

Parameters:

actor - Actor under analysis.

numSpan - The size of the span to expand the variable domain.

Returns:

The set of variables (variable names) used in the FSMActor.

Throws:

IllegalActionException

_enumerateStateSet

private static java.util.HashSet<State> _enumerateStateSet(FSMActor actor)
                                                    throws IllegalActionException

Perform an enumeration of the state in this actor and return the name of the states. It seems to have a better way to do this (a mechanism to enumerate using existing member functions).

Parameters:

actor - The actor under analysis

Returns:

The set of states of the FSMActor.

Throws:

IllegalActionException

_enumerateString

private static java.util.ArrayList<java.lang.String> _enumerateString(int index,
                                                                      java.util.ArrayList<java.lang.String> paraEnumerateString)

This private function generates all possible combinations of string with length i with character 0 and 1. For example, for i = 2 it would generate {00, 01, 10, 11}. This is designed to invoke recursively to achieve this goal.

Parameters:

index - The size of the index.

paraEnumerateString - Existing strings that need to be attached.

Returns:

An list of all possible combination for char 0 and 1 of size index.

_generateTransition

private static java.util.ArrayList<REDUtility.REDTransitionBean> _generateTransition(FSMActor actor,
                                                                                     State state,
                                                                                     java.util.HashSet<java.lang.String> variableSet,
                                                                                     java.util.HashSet<java.lang.String> globalSynchronizerSet)
                                                                              throws IllegalActionException

This private function is used to generate the transition description for a certain state in a certain actor. The output format is CTA acceptable by model checker RED.

Parameters:

actor - Actor under analysis

state - State under analysis

variableSet -

globalSynchronizerSet - Set of useful synchronizers. There are some synchronizers which is not useful. They are not connected to/from a valid actor where analysis is possible.

Returns:

A set of transition descriptions packed in a list.

Throws:

IllegalActionException

_retrieveVariableInitialValue

private static java.util.HashMap<java.lang.String,java.lang.String> _retrieveVariableInitialValue(FSMActor actor,
                                                                                                  java.util.HashSet<java.lang.String> variableSet)

A private function for generating initial values for the initial variable set. The current approach is to retrieve them from the parameter specified in the actor.

Parameters:

actor -

variableSet -

Returns:

The variable initial value set.

_rewriteModalModelWithStateRefinementToFSMActor

private static FSMActor _rewriteModalModelWithStateRefinementToFSMActor(ModalModel modalmodel)
                                                                 throws IllegalActionException,
                                                                        NameDuplicationException,
                                                                        java.lang.CloneNotSupportedException

This is an experimental function which analyzes a ModalModel and flatten it into a single FSMActor. As model checkers in timed systems are using models without hierarchy, this function is required.

In our current implementation we only allow one additional layer for the refinement. Also the additional layer must be a finite state refinement so that the conversion is possible. But it is easy to expand this functionality into multiple layer.

Note that in the current context of ModalModel, when state machine refinement is used, it is not possible to generate further refinements, meaning that the current implementation is powerful enough to deal with state refinements.

Parameters:

modalmodel - Whole System under analysis.

Returns:

Equivalent FSMActor for later analysis.

Throws:

IllegalActionException

NameDuplicationException

java.lang.CloneNotSupportedException

_translateBBNondeterministicDelayedActor

private static REDUtility.REDSingleEntityBean _translateBBNondeterministicDelayedActor(BoundedBufferNondeterministicDelay delayedActor,
                                                                                       java.lang.String inputSignalName,
                                                                                       java.lang.String outputSignalName)
                                                                                throws IllegalActionException

Translate a bounded buffer, nondeterministic delayed actor.

Parameters:

delayedActor - The actor.

inputSignalName - The input signal

outputSignalName - The output signal

Returns:

description of the TimedDelayActor acceptable by model checker RED.

Throws:

IllegalActionException - If the delay or bufferSize parameters of the delayedActor cannot be read.

_translateBBTimedDelayedActor

private static REDUtility.REDSingleEntityBean _translateBBTimedDelayedActor(BoundedBufferTimedDelay delayedActor,
                                                                            java.lang.String inputSignalName,
                                                                            java.lang.String outputSignalName)
                                                                     throws IllegalActionException

This is an utility function which performs the translation of a single TimedDelay actor into the format of communicating timed automata (CTA) acceptable by model checker RED.

Parameters:

delayedActor - actor which needs to be converted

inputSignalName - The name of the input signal. This must be derived externally.

outputSignalName - The name of the output signal. This must be derived externally.

Returns:

description of the TimedDelayActor acceptable by model checker RED.

Throws:

IllegalActionException

_translateClockActor

private static REDUtility.REDSingleEntityBean _translateClockActor(Clock clockActor,
                                                                   java.lang.String outputSignalName)
                                                            throws IllegalActionException

This is an utility function which performs the translation of a single clock actor into the format of communicating timed automata (CTA) acceptable by model checker RED.

Parameters:

clockActor - The actor which requires to be converted.

outputSignalName - The name of the output signal. This must be derived externally.

Returns:

clock description acceptable by model checker RED.

Throws:

IllegalActionException

_translateFSMActor

private static REDUtility.REDSingleEntityBean _translateFSMActor(FSMActor actor,
                                                                 int span,
                                                                 java.util.HashSet<java.lang.String> globalSynchronizerSet)
                                                          throws IllegalActionException

Translate an FSM actor.

Parameters:

actor - The actor to be translated.

span - The size of the span to expand the variable domain. This variable is used to determine the inner variables used by an actor

globalSynchronizerSet - The set of useful synchronizers. There are some synchronizers which is not useful. They are not connected to/from a valid actor where analysis is possible.

Returns:

description of the TimedDelayActor acceptable by model checker RED.

Throws:

IllegalActionException - If thrown while getting the initial state of the actor, deciding the guard signal variable set or generating transitions.

_translateTimedDelayedActor

private static REDUtility.REDSingleEntityBean _translateTimedDelayedActor(TimedDelay delayedActor,
                                                                          java.lang.String inputSignalName,
                                                                          java.lang.String outputSignalName,
                                                                          int bufferSize)
                                                                   throws IllegalActionException

This is an utility function which performs the translation of a single TimedDelay actor into the format of communicating timed automata (CTA) acceptable by model checker RED.

Parameters:

delayedActor - actor which needs to be converted

inputSignalName - The name of the input signal. This must be derived externally.

outputSignalName - The name of the output signal. This must be derived externally.

bufferSize - The defined buffer size used in verification

Returns:

description of the TimedDelayActor acceptable by model checker RED.

Throws:

IllegalActionException