Portal:Tutorials

From Verification Body of Knowledge
Jump to navigation Jump to search

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


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.