Difference between revisions of "Portal:Tutorials"

From Verification Body of Knowledge
Jump to navigation Jump to search
 
(3 intermediate revisions by one other user not shown)
Line 1: Line 1:
;Verification Tools & Processes 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 Tools & Processes Tutorials
== 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


;Verification of Autonomous Systems Tools & Processes Tutorials


* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]
* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]
Line 28: Line 49:
       theta' = thetadt,  
       theta' = thetadt,  
       thetadt' = (K*R^2)/(J+m*R^2)*theta + (K*R)/(J+m*R^2)*u  
       thetadt' = (K*R^2)/(J+m*R^2)*theta + (K*R)/(J+m*R^2)*u  
       & theta >=0}};
       & theta >=0}};
 
  End.  
  End.  
  ProgramVariables
  ProgramVariables
Line 41: Line 61:
  End.
  End.


;KeymaeraX DrivelineDynamics
  ArchiveEntry "DrivelineDynamics"
  ArchiveEntry "DrivelineDynamics"
  Definitions  
  Definitions  
   Real Jf = 0.625;
   Real Jf = 0.625;
Line 53: Line 73:
   Real K2 = 57.1911;
   Real K2 = 57.1911;
   Real K3 = -12.9458;
   Real K3 = -12.9458;
 
   HP ctrl ::= {u := -(K1*Weng + K2*Wwheel + K3*phi);};
   HP ctrl ::= {u := -(K1*Weng + K2*Wwheel + K3*phi);};
 
   HP driveline ::= {{
   HP driveline ::= {{
       Weng' = (1/Jf)*(u - (1/r)*(cs*phi + ds*((Weng/r)-Wwheel))),
       Weng' = (1/Jf)*(u - (1/r)*(cs*phi + ds*((Weng/r)-Wwheel))),
Line 63: Line 81:
    
    
  End.  
  End.  
  ProgramVariables
  ProgramVariables
   Real Weng;      /*engine speed*/
   Real Weng;      /*engine speed*/
Line 70: Line 87:
   Real u;          /*control input*/
   Real u;          /*control input*/
  End.  
  End.  
  Problem
  Problem
     Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0
     Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0
  End.
  End.
  End.
  End.

Latest revision as of 12:57, 17 May 2022

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.