Package net.maswag.falcaun

Class BlackBoxVerifier<I>

java.lang.Object
net.maswag.falcaun.BlackBoxVerifier<I>
Type Parameters:
I - The type of input symbols at each step.
public class BlackBoxVerifier<I> extends Object
Verifies a black-box system against specified properties using various equivalence oracles and model checking techniques.

This class provides a comprehensive framework for verifying the behavior of a black-box system by comparing it against a set of Signal Temporal Logic (STL) properties. It utilizes learning algorithms, equivalence oracles, and model checkers to identify any discrepancies between the expected and actual behaviors of the system.

Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

    • EDGE_PARSER

      private static final Function<String,String> EDGE_PARSER

    • memOracle

      MembershipOracle.MealyMembershipOracle<String,String> memOracle
      The membership oracle used to evaluate test cases and provide the system's output for given inputs.

    • verifiedSystem

      private final SUL<String,String> verifiedSystem
      The System Under Learning (SUL) representing the black-box system to be verified.

    • learnedMealy

      private net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> learnedMealy
      The learned Mealy machine that models the behavior of the black-box system based on test cases.

    • cexMealy

      private List<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> cexMealy
      A list of Mealy machines representing counterexamples found during the verification process.

    • inputAlphabet

      private final net.automatalib.alphabet.Alphabet<String> inputAlphabet
      The alphabet of input symbols used in the verification process.

    • learner

      private final LearningAlgorithm.MealyLearner<String,String> learner
      The learning algorithm used to learn the behavior of the black-box system from test cases.

    • eqOracle

      private final MealyEQOracleChain<String,String> eqOracle
      The equivalence oracle used to find counterexamples by comparing the learned model with the black-box system.

    • properties

      private final AdaptiveSTLUpdater<I> properties
      The adaptive STL updater that manages and updates the Signal Temporal Logic (STL) properties to be verified.

    • cexInput

      private List<net.automatalib.word.Word<String>> cexInput
      A list of input words that led to counterexamples found during the verification process.

    • cexProperty

      private List<TemporalLogic<I>> cexProperty
      A list of Signal Temporal Logic (STL) properties that were violated by the counterexamples found during the verification process.

    • cexOutput

      private List<net.automatalib.word.Word<String>> cexOutput
      A list of output words produced by the black-box system for the counterexamples found during the verification process.

    • modelChecker

      private final net.automatalib.modelchecking.ModelChecker.MealyModelChecker<String,String,String,net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> modelChecker
      The model checker used to verify the learned Mealy machine against Signal Temporal Logic (STL) properties.

    • timeoutOracles

      private final List<TimeoutEQOracle<String,String>> timeoutOracles
      A list of timeout oracles used to manage timeouts for equivalence oracle operations.

    • timeout

      private Long timeout
      The timeout value in seconds used for equivalence oracle operations.

  • Constructor Details

  • Method Details

    • addWpMethodEQOracle

      public void addWpMethodEQOracle(int maxDepth)

    • addBFOracle

      public void addBFOracle(double multiplier)

    • addRandomWordEQOracle

      public void addRandomWordEQOracle(int minLength, int maxLength, int maxTests, Random random, int batchSize)

    • addRandomWalkEQOracle

      public void addRandomWalkEQOracle(double restartProbability, long maxSteps, Random random)

    • addCompleteExplorationEQOracle

      public void addCompleteExplorationEQOracle(int minDepth, int maxDepth, int batchSize)

    • addCornerCaseEQOracle

      public EvaluationCountable.MealyEquivalenceOracle<String,String> addCornerCaseEQOracle(int length, int minStep)
      Add a corner case equivalence oracle.

      This oracle tries the corner case input, i.e., the inputs with the same values

      Parameters:
      length - The length of the input.
      minStep - The minimum step of the corner case.

    • addEqOracle

      public void addEqOracle(EquivalenceOracle.MealyEquivalenceOracle<String,String> eqOracle)

    • setTimeout

      public void setTimeout(long timeout)
      Set timeout to the equivalence oracle added next time.
      Parameters:
      timeout - timeout in seconds.

    • run

      public boolean run()
      Returns:
      Returns true if and only if the given black-box system is verified i.e., no counter example is found.

    • writeDOTCex

      public void writeDOTCex(int index, Appendable a) throws IOException
      Wirte the DOT of the found counter example.
      Parameters:
      a - Write the DOT to a
      Throws:
      IOException - The exception by GraphDOT.write

    • writeDOTLearnedMealy

      public void writeDOTLearnedMealy(Appendable a) throws IOException
      Wirte the DOT of the learned Mealy machine.
      Parameters:
      a - Write the DOT to a
      Throws:
      IOException - The exception by GraphDOT.write

    • visualizeCex

      public void visualizeCex(int index)
      Visualize the found counter example.

    • visualizeLearnedMealy

      public void visualizeLearnedMealy()
      Visualize the learned Mealy machine

    • writeETFLearnedMealy

      public void writeETFLearnedMealy(OutputStream os)
      Write the ETF of the learned Mealy machine.
      Parameters:
      os - Write the ETF to os

    • processMealy

      private boolean processMealy()
      Set the counter example input/output.
      Returns:
      Returns true if and only if the black-box system is verified i.e., no counter example is found for any system.