Model checker (Prototype)

Prototype of three explicit state model checker for Scala-Futures, ZIO and a subset of akka typed.

Why? Model checking allows to tests for race conditions and similar problems that arise in concurrent programs. Something that is notorious difficult with normal tests. This projects enables the power of model checking for Scala programs.

See the examples in tests:

• Scala future
• ZIO
• akka-typed

Features

• finds race conditions
• produces trace to debug errors
• works on multiple JDK versions
• nice DSL to express advanced concepts
• finds bugs in non terminating programs (akka only)

Known limitations:

• relies upon the assumption that the tested program don't invoke more side effects than expected

Install

Currently this project isn't publish on maven central or any other repository. So you need to build it your self.

To publish it locally on your machine run sbt +publishLocal. Add the following lines to your project:

libraryDependencies ++= Seq(
  "jentsch.berlin" %% "modelchecker-futures" % "0.1.0-SNAPSHOT" % Test,
  "jentsch.berlin" %% "modelchecker-zio" % "0.1.0-SNAPSHOT" % Test,
  "jentsch.berlin" %% "modelchecker-akka" % "0.1.0-SNAPSHOT" % Test
)

This will enable all three model checkers in the tests of your project. If you would prefer this on maven central, feel free to create a PR - until now this wasn't necessary for this prototype.

Development

This sbt project is separated into six sub projects:

• futures contains a model checker for scala Futures and their ExecutionContext
• zio contains a model checker for zio
• akka contains a model checker for Akka
• core contains shared functionality of futures, akka, and zio project
• benchmarks helps to justify performance sensitive decisions
• jpf helps to compare this project to Java Pathfinder

IntelliJ and Metals should be able to pick up the sbt configuration of the project.

Tests

Use sbt test to execute all tests.

This project has three different kinds of tests.

Doc-Examples

Notice that example code snippets from scaladoc with sbt-example are used to test functionality. For those tests ScalaTest with Matchers is used.

An example:

/**
  * @example My little object. 
  * {{{
  *   MyObject.x should be(1)
  * }}}
  */
object MyObject {
  val x = 1
}

Regression tests

In some cases the behaviour of the system isn't covered by the doc-examples and a bug occure. For such cases a regular test in <sub-project>/test/scala/... describes the correct behaviour.

Additionally some uses cases are also part of the test suite and live under <sub-project>/test/scala/.../example/.

Documentation

The main source of information is currently the api-documentation generated by scaladoc and the above mentioned examples in test.

Alternatives

The many more model checker out there. As far as I'm aware only the Java Pathfinder can consume Java-Programs.