=== Modbat: Model-based Tester === Modbat is specialized to testing the application programming interface (API) of software. The model used by Modbat is compatible with Java bytecode. The user defines and compiles a model, which is then explored by Modbat and executed against the system under test. Failed test runs are reported as an error trace. --- Installation --- Requirements: Scala 2.9 or higher (tested on 2.9.2). The distribution comes with two JAR files: modbat.jar and modbat-examples.jar. The first file is an executable JAR file that has to be run using the Scala runtime environment. The second file is optional and contains examples. --- Basic usage --- scala modbat.jar [OPTIONS] MODELCLASS... For help, try scala modbat.jar -h and to check the current configuration, use scala modbat.jar -s The second file contains examples and a model template; unpack that file using jar xf modbat-examples.jar The examples are contained in modbat-examples/test, while the template is in modbat-examples/ModelTemplate.scala. --- How to run the examples --- Usage is as above. The examples can be run either from the JAR file examples.jar, or using the class files from the unpacked JAR file. In either case, the examples must reside in the classpath as set by CLASSPATH or given by option --classpath (note: two dashes): Example: (1) With the examples provided as a JAR file: scala modbat.jar --classpath=modbat-examples.jar modbat.test.SimpleModel (2) If the contents of modbat-examples.jar are unpacked: scala modbat.jar --classpath=. modbat.test.SimpleModel The model is explored non-deterministically. By default, 50 runs on the model are executed, and all failing traces are written to a file (one file for each trace). The defaults are set such that you do usually not have to change them; options that may be of interest are "-n", "-s", "--mode", "stop-on-failure". Run scala modbat.jar -h for more information. --- How to read the error trace --- If a model run causes an assertion violation or other unhandled exception, an error trace is generated in a .err file. The name of the .err file (without the extension .err) corresponds to the random seed used for that failed test run. To re-run the failed test without logging the output to a file, use scala modbat.jar -n=1 -s= --no-redirect-out Example: scala modbat.jar -n=1 -s=2455cfe modbat.test.SimpleModel \ --no-redirect-out --- Semantics of model --- The model is given as an "extended finite state machine" in a domain-specific language that is embedded in Scala. Basic transitions between two states are given as "pre" -> "post" Most transitions will have a transition function attached to them, using ":=" "pre" -> "post" := { // Scala code } Any Scala code is allowed, but preconditions have a special semantics: Exploration of the model backtracks if a precondition is violated. Therefore, all preconditions should be stated at the beginning of a transition function, and be side-effect-free: "pre" -> "post" := { require (x < 0) } A model will contain multiple transitions, separated by a comma, as shown in modbat/ModelTemplate.scala. --- Advanced features --- Advanced exception handler constructs can be attached to a transition function. These are: * choose(min, max): Returns a random number between min (inclusive) and max (exclusive). * throws: "pre" -> "post" := { codeThrowingException } throws("IOException", "SecurityException") "throws" specifies that an exception must always occur in that transition; the absence of an exception is regarded as an error. A list of exception types, given as strings, is supported. * catches: "pre" -> "post" := { codeWithPossibleException } catches("Exception" -> "handlerState") "catches" deals with non-deterministic exceptions that may occur, but are not always expected. Input/output errors can be handled in the model in this way. A "catches" statement supports a list of comma-separated (exceptionType -> handlerState) pairs, given as strings. * nextIf: "pre" -> "post" := { n = choose(0, 40) } nextIf({ () => n > 30 } -> "nextState") Non-deterministic conditions other than exceptions can be handled using "nextIf"; given a list of (condition, nextState) pairs, the transition branches to "nextState" if the given condition is true. Conditions are usually given as an anonymous function in Scala, using the "() =>" notation, before the actual condition. * maybe: "pre" -> "post" := { maybe (doSomething) } An action is only executed with a certain probability (default: 0.5). If a random number between 0 and 1 exceeds that probability, then the function is not executed. * maybeBool: Same as "maybe" but returns a boolean. If the function is not executed (due to the given probability not being fulfilled), false is returned. * maybeNextIf: "pre" -> "post" := { n = choose(0, 40) } maybeNextIf({ () => n > 30 } -> "nextState") Same as "nextIf", but the condition is only evaluated with a certain probability (default: 0.5). Otherwise, the given condition is ignored, and the default transition is chosen. This function is syntactic sugar for nextIf({ () => maybeBool({ () => n > 30 }) } -> "nextState") --- Singleton models vs instance models --- Modbat allows a model to be defined inside "object model" or "class model". The former generates a singleton model, corresponding to a "static" instance in Java. It has only one set of variables that is initialized at model initialization time (before the first test case is executed). If a variable needs to be initialized before each test, this has to be done either using a helper method, or with an extra transition from the initial state to an "initialized" state. A "class model" is an instance of that class, so it is always automatically instantiated and initialized before each test run. The "default instance" is either the first instance that is generated from the given class model, or the static instance in case a singleton model is used. An instance model can also be "launched" to run concurrently with the default instance. Unlike the instance model, a launched model can take arguments in its constructor and therefore be launched in a different state than the default instance. Launched instances (including the default instance) are executed in parallel, using stepwise interleaving. In other words, the order in which multiple available transitions from different instances are executed is non-deterministic, but actions of different instances are not interleaved. Therefore, model actions always appear to be executed atomically against actions of other instances. --- Helper method annotations --- Modbat supports several method annotations: * @init: The given method is executed before the first test is run, but not before each test. This is useful, for example, to execute a server instance for testing client-side behavior, as is done in model modbat.test.JavaNioSocket. * @shutdown: This method is executed after the last test completes, or when Modbat is forcibly shut down by signal TERM. * @before: This action is execute before each test is executed, but not when a new instance model is launched. This annotation therefore allows a differentiation between the need to initialize data before each test (using the annotation) or before a model instance is executed (using an initialization transition preceding the actual functionality of the model). The action is executed on the default instance of the model. * @after: This action is executed after each test execution run, on the default instance of the model. --- Visualization --- The tool supports a basic visualization (requiring graphviz), using scala modbat.jar --mode-dot --dot-file= --- How to compile your own model --- It is recommended that you copy ModelTemplate.scala to create your own model. Compilation of a model requires modbat.jar in the classpath. For a model defined in "Model.scala", and modbat.jar in the current directory, use: scalac -cp modbat.jar Model.scala --- Troubleshooting --- At this stage, many problems encountered are class path/class loader issues. Please check the following: * CLASSPATH setting. * Use "scala modbat.jar --classpath=..." to override this setting. * Note that any CLASSPATH setting or -cp/-classpath argument to scala itself is ignored when using an executable JAR file. If modbat.jar is not found, use the correct (full) file name, regardless of CLASSPATH, as that setting is ignored by the Scala runtime environment (which is the Java Virtual Machine). * Modbat itself checks for the CLASSPATH setting, and uses it; however, the syntax of --classpath uses two dashes, not one.