Portal:Tutorials

Verification-Focused Tools & Processes Tutorials

• Requirements and Specifications
• Assurance Case Construction
• Formal Models & Methods
  • Model Checking
• Simulators and Modelling Tools
• Sample-based Testing
• Hardware Testing
• Run-Time Verification and Monitoring

Autonomy-Focused Tools & Processes Tutorials

• Autonomy Architectures and Middlewares
  • ROS
  • MOOS
  • CARACaS
• Domain-Specific Languages
  • PDDL
• Messaging Standards
  • ??
• System Design and Modeling Tools / Approach / Process
  • Finite State Machines
  • Automata
    • Many types!
  • MDPs and POM-DPs
  • Model-Based Systems Engineering

• Andre Platzer Tutorial on how to use Keymaera-X

KeyMaeraX - Garage Door

ArchiveEntry "Garage Door"
Definitions 
 Real m = 50;
 Real k = 600; 
 Real K = 0.6; 
 Real R = 0.005; 
 Real J = 0.02;
 Real Kp = 240; 

 Real error(Real ref, Real theta) = (ref - theta); 
 
 HP ctrl ::= {u := Kp*error;};
 
 HP motion ::= {{
     theta' = thetadt, 
     thetadt' = (K*R^2)/(J+m*R^2)*theta + (K*R)/(J+m*R^2)*u 
     & theta >=0}};  
End. 
ProgramVariables
 Real theta;       /*position*/
 Real thetadt;     /*velocity*/
 Real u;           /*control input*/
End. 
Problem
   theta > 0 -> [{ctrl; motion;}*] theta >= 0
End.
End.

KeymaeraX DrivelineDynamics

ArchiveEntry "DrivelineDynamics"
Definitions 
 Real Jf = 0.625;
 Real Jc = 6250; 
 Real cs = 65000; 
 Real ds = 1000; 
 Real Tload = 7000;
 Real r = 12.5; 
 Real K1 = 5.4567;
 Real K2 = 57.1911;
 Real K3 = -12.9458;
 HP ctrl ::= {u := -(K1*Weng + K2*Wwheel + K3*phi);};  
 HP driveline ::= {{
     Weng' = (1/Jf)*(u - (1/r)*(cs*phi + ds*((Weng/r)-Wwheel))),
     Wwheel' = (1/Jc)*(cs*phi + ds*((Weng/r)-Wwheel)-Tload),
     phi' = (Weng/r) - Wwheel 
 }};
 
End. 
ProgramVariables
 Real Weng;       /*engine speed*/
 Real Wwheel;     /*wheel speed*/
 Real phi;        /*torsion*/
 Real u;          /*control input*/
End. 
Problem
   Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0
End.
End.