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.
- MathematicalSystems.jl Systems definitions in Julia.
- SX.jl SpaceEx modeling language parser.
- BernsteinExpansions.jl A Julia package to compute Bernstein coefficients of multivariate polynomials.
- IntervalMatrices.jl Matrices with interval coefficients in Julia.
- MathematicalSets.jl Set definitions in Julia.
- RangeEnclosures.jl A Julia package to compute range enclosures of real-valued functions.
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.
Nonlinear dynamics of a quadrotor: verifying stabilization with a PD controller
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))
Transition into aborting mode of the linear hybrid spacecraft rendez-vous model
# 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)
Platoon of three vehicles following each other with loss of communication
Two-dimensional switched oscillator and a parametric number of filters (here 256)
Structural model of component 1R (Russian service module) with 270 state variables
Benchmarks & Repeatability Evaluations
- 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.
- Marcelo Forets. Universidad de la República, Uruguay.
- Christian Schilling. Institute for Science and Technology, Austria.
Contributors to JuliaReach projects
- Aadesh Deshmuhk. Indian Institute of Information Technology, India.
- Bruno Garate. Universidad de la República, Uruguay.
- Sebastián Guadalupe. Universidad de la República, Uruguay.
- Nikolaos Kekatos. Université Grenoble Alpes, France.
- Benoit Legat. UCLouvain, Belgium.
- Kostiantyn Potomkin. Australian National University, Australia.
- Alexandre Rocca. INRIA Grenoble, France.
- Frédéric Viry. CERFACS, France.
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.