org.objectweb.dsrg.sofa.cushion.behavior.ebp2prom
Class EBP2PromChecker

java.lang.Object
  extended by org.objectweb.dsrg.sofa.cushion.behavior.CheckerImpl
      extended by org.objectweb.dsrg.sofa.cushion.behavior.ebp2prom.EBP2PromChecker
All Implemented Interfaces:
org.objectweb.dsrg.sofa.util.checker.Checker

public class EBP2PromChecker
extends CheckerImpl

This is implementation of the Checker interface for EBP2Promela case.

Author:
kofron

Nested Class Summary
 
Nested classes/interfaces inherited from class org.objectweb.dsrg.sofa.cushion.behavior.CheckerImpl
CheckerImpl.InvalidBindingTypeException
 
Constructor Summary
EBP2PromChecker()
          Creates a new instance of EBP2PromChecker
 
Method Summary
protected  java.lang.String getBehaviorType()
           
protected  org.ow2.dsrg.fm.ebp2promela.architecture.EBPParserBridge getParserBridge()
           
 org.objectweb.dsrg.sofa.util.checker.CheckingResult checkArchitecture(org.objectweb.dsrg.sofa.repository.model.Architecture arch, java.io.PrintStream out)
          Performs the behavior verification of Extended Behavior Protocols via translation to Promela and using the Spin model checker (www.spinroot.com)
 
Methods inherited from class org.objectweb.dsrg.sofa.cushion.behavior.CheckerImpl
getFrame, getProtocol, parseArch, printStream
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

EBP2PromChecker

public EBP2PromChecker()
Creates a new instance of EBP2PromChecker

Method Detail

getParserBridge

protected org.ow2.dsrg.fm.ebp2promela.architecture.EBPParserBridge getParserBridge()
Specified by:
getParserBridge in class CheckerImpl

checkArchitecture

public org.objectweb.dsrg.sofa.util.checker.CheckingResult checkArchitecture(org.objectweb.dsrg.sofa.repository.model.Architecture arch,
                                                                             java.io.PrintStream out)
Performs the behavior verification of Extended Behavior Protocols via translation to Promela and using the Spin model checker (www.spinroot.com)


getBehaviorType

protected java.lang.String getBehaviorType()
Specified by:
getBehaviorType in class CheckerImpl
Returns:
the used behavior type