Meeting Minutes - Artem1199/ECE-HACoSR2 GitHub Wiki

Galois Inc Meetings 2 (January 28th, 2020)

Note on PDS;

• Introduction is unclear on what this project is

What questions do we have for this PDS?

• The PDS looks good
• Do we need written approval, will an email work?
• Good start and plan for the year
• Sliding mode controller instead of non-linear controller is a good idea

Professor recommended sliding mode controller.

• Still has an adaptive method

For Kind2

• Install Nix package and use NIX
• Use Ocaml 4.0.4

Lustre to Rust

• Boiler plate, harness to run Cargo

DockerHub Kind2 work well

Equivalence checking on the Rust library

• Implement your own few lines of code for the PID controller
• You could use an online PID library aswell
• Library to can used as an example to start and compared to lustre generator
• • (PID_control 7.2)
• • Reset property an we can verify
• • Potentially used to reduce the into the a system after an idle

Galois does not want to see the schedule.

Galois Inc Meetings 1 (December 17th, 2019)

Leverage formal verification, control, on an embedded device

Dive into control design and verification

• Hardware Design
• Design Software
• Traceability that the design matches the code base

We will use tools that have not been used for controls before

Embedded Device + Rust Complication will be used

Agenda

• Meet after the requirements document.

• Available resources are there
• more research will be necessary

Modify Lustre/Kind2 Rust code generator to generate embedded Rust

• Simulator dynamics of the robot
• Test on the robot each time

Lustre

• Stream or flow language
• Stream of data comes in and comes out
• You can ask questions about the model(prior state)
• Pre-command
• How a system evolves over time
• Currently it's for a stand alone simulation
• properties on model should be on the code

Linear or Discrete math is the limit

• Lean can handle more math

Start w/ something small for a PID controller -quickcheck static check

• • used to verify properties on a model

Start with a linear controller

• multiple gain, linear, or non linear

Non-Linear Controller

• We use a standard depository, commit to it early and often
• Use Github issues for things that are unclear

Verification a property that should hold for all domains.

Given this property is there an initial condition that would cause failure

• Handbook of model checking can help

Robot information

• Sampling + Statistical method
• Yaw, tilt, torque
• Test will my design create a stable controller
• • Stable vs. Oscillating, we don't want to move and don't want it to be unstable

Stable vs. Robust

Ideas

• BangBang controller for motor deadzone
• Sliding mode controller
• MPU
• Motor encoders

Task 1

• Replace controller and recompile on new processor
• Think about VCR