Package net.maswag.falcaun
package net.maswag.falcaun
FalCAuN - Falsification tool for Cyber-Physical Systems via Automata Learning.
This is the core package of FalCAuN, which provides the fundamental components for falsification of cyber-physical systems using automata learning techniques.
FalCAuN implements various temporal logics, signal mappers, and equivalence oracles to enable effective falsification of complex systems.
-
ClassDescriptionAbstract class representing a potentially adaptive set of Signal Temporal Logic (STL) formulas.Abstract class representing an Input-Output (IO) signal.Abstract class for reading and parsing mapper data from files.Abstract class for implementing equivalence oracles that select test cases based on a cost function.Adaptive updater of STL/LTL formulasInterface for a potentially adaptive set of Signal Temporal Logic (STL) formulas.Utility class for constructing abstract atomic propositions.Verifies a black-box system against specified properties using various equivalence oracles and model checking techniques.Continuous-time systems under learning with numerical I/O.This class provides construction of Mealy machine from DOT fileSimulinkGenerationalGeneticAlgorithm class.EQSearchProblem class.SimulinkSteadyStateGeneticAlgorithm class.A pair of input and output signals at one time step potentially with some previous output signals.Class to construct pseudo signals from concrete signalsEquivalence query using genetic algorithmEnumeration of selection methods used in Genetic Algorithm (GA) equivalence queries.HillClimbingEQOracle class.A class that represents a mapping from characters to double values.Deprecated.This class implements a random mutation operator for integer solution.Uniform crossover for integersA signal with continuous output values.A discrete-time signal with both input and output values.IOSignal<I>A signal with both input and output values.Represents a pair of input and output signals at one time step in a system's behavior.Represents the atomic propositions (APs) for LTL formulas.Base class for LTL formula implementations that provides common functionality for atomic propositions management using composition instead of inheritance.Equivalence oracle that uses a fixed set of samples.MutateSelectEQOracle class.The membership oracle for a Simulink modelA membership oracle that computes the cost of input-output signals using a specified cost function.Systems under learning with numerical I/O.I/O Mapper between abstract/concrete NumericSUL.Output Mapper for NumericSUL based on Specification-Guided Abstraction.Verifies a Numeric System Under Learning (NumericSUL) against specified properties using various equivalence oracles and model checking techniques.A class for mapping output values to characters.Deprecated.Use
OutputMapperinstead.SignalDiscretizer post-composed with an SULMapper.SignalDiscretizer pre-composed with an SULMapperAnswer the Equivalence query by simulated annealingOutput Mapper for Mealy machine based on Specification-Guided Abstraction.Signal is a sequence of values, each associated with an increasing timestamp.I/O Mapper between abstract/concrete signals using InputMapper and OutputMapper.Signal derivation mapper that uses SignalMapper to derive signals from concrete I/O signals.Interface to construct pseudo signals from concrete signalsClass to construct pseudo signals from concrete signalsList of STL/LTL formulas without updateStopDisprovedEQOracle<I,O, C> Wraps an equivalence oracle so that the equivalence oracle is skipped if all the LTL oracles are disproved.Time measurement utility for tracking elapsed time in nanoseconds.TimeoutEQOracle<I,O> Am equivalence oracle to add timeout in addition to the original oracle.A sequence of values each associated with an increasing timestamp.Equivalence Oracle using the actual model of SUL.
InputMapperinstead.