JuliaReach is a toolbox for set-based reachability analysis and safety verification of dynamical systems. The choice of the programming language Julia and the accompanying documentation of the packages allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages.

For more information see the publications page. Works using JuliaReach related projects can be found in the citations page.

The core JuliaReach packages are Reachability.jl, with state-of-the-art implementationss of reachability algorithms for continuous and hybrid systems, either linear or nonlinear. The initial value problems are stated using the MathematicalSystems.jl library, a project also maintained by the JuliaReach org.

LazySets.jl is the key standalone library for calculus with convex sets, and it can be used to represent and compute with sets and operations between sets that are either concretey or lazily represented, or in mixed representations, where lazy stands for the ability to delay set computations until they are needed.

  • LazySets.jl A Julia package for calculus with convex sets.
  • Reachability.jl Reachability and Safety of Nondeterministic Dynamical Systems.

The following component packages are developed and maintained by the JuliaReach org.

If you like some of these packages, consider contributing! Create an issue in the GitHub issue tracker to report a bug, open a discussion about existing functionality, or suggest new features.

If you have written code and would like it to be peer reviewed and added to the library, you can make fork and send a pull request. Typical contributions include fixing a bug, adding a new feature or improving the documentation (either in source code or the online manual). The JuliaReach Developer's guide describes coding guidelines; take a look when in doubt about the coding style that is expected for the code that is finally merged into the library.

You are also welcome to get in touch with us in the JuliaReach gitter chat , where technical discussions take place.

We study the dynamics of a quadrotor as derived in [R. Beard. Quadrotor dynamics and control]. The variables required to describe the model are the inertial (north) position, the inertial (east) position, the altitude, the longitudinal velocity, the lateral velocity, the vertical velocity, the roll angle, the pitch angle, the yaw angle, the roll rate, the pitch rate, and the yaw rate. To check interesting control specifications, we stabilize the quadrotor using simple PD controllers for height, roll, and pitch.

The specification consists of changing the height from 0 [m] to 1 [m] within 5 [s]. A goal region [0.98, 1.02] of the height has to be reached within 5 [s] and the height has to stay below 1.4 for all times. After 1 [s] the height should stay above 0.9 [m]. The initial position of the quadrotor is uncertain in all directions within [0.4, 0.4] [m]. The initial velocity is uncertain within [0.4, 0.4] [m/s] for all directions. All other values are initialized as 0.

using Reachability, LazySets

# load quadrotor model, parameters and safety property
include("~/ReachabilityBenchmarks/models/ARCH/NLN/Quadrotor/quadrotor.jl")

# nonlinear equations x' = f(x(t))
𝐹 = BlackBoxContinuousSystem(quadrotor!, 12)

# initial set (positions, velocities and roll, pitch and yaw angles)
ΔX0 = [0.4, 0.4, 0.4, 0.4, 0.4, 0.4, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
X0 = Hyperrectangle(zeros(12), ΔX0)

# instantiate the initial value problem with a set of initial conditions
𝑃 = InitialValueProblem(𝐹, X0)

# problem options (plot variables: 0 -> time, 3 -> height)
𝑂 = Options(:T=>5.0, :plot_vars=>[0, 3],
            :property=>height_control, :project_reachset=>true)

# set algorithm-specific options for TaylorModels method
𝑂jets = Options(:abs_tol=>1e-7, :orderT=>5, :orderQ=>1, :max_steps=>500)

# solve the reachability problem
sol = solve(𝑃, 𝑂, op=TMJets(𝑂jets))
# load spacecraft rendez-vous model
include("~/ReachabilityBenchmarks/models/ARCH/AFF/SpacecraftRendezvous.jl")

# instance of the model with a given time range of abort mission
SRA02, options = spacecraft(abort_time=[120., 125.])

# continuous post-operator using decomposition-based approach
opC = BFFPSV18(:partition => [1:5], :δ => 0.04)

# discrete post-operator with lazy intersections
opD = LazyDiscretePost(:lazy_R⋂I => true, :lazy_R⋂G => true)

options[:mode] = "check"
options[:plot_vars] = [1, 2]
options[:project_reachset] = true

# verify the safety property
solve(system, options, opC, opD)
using Reachability
using Reachability
using Reachability
using Reachability
  • ReachabilityBenchmarks. Repository with benchmark evaluations of reachability problems.
  • ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems.
  • HSCC19. 22nd ACM International Conference on Hybrid Systems: Computation and Control.
  • ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems.

Lead developers

Contributors to JuliaReach projects

Scientific collaborators network

  • Luis Benet. Instituto de Ciencias Físicas, Universidad Nacional Autónoma de México, México.
  • Sergiy Bogomolov. College of Engineering & Computer Science, Australian National University, Australia.
  • Goran Frehse. ENSTA ParisTech, France.
  • Andreas Podelski. University of Freiburg, Germany.
  • David P. Sanders. Departamento de Física, Facultad de Ciencias, Universidad Nacional Autónoma de México, México.