Difference between revisions of "Portal:Tutorials"
Jump to navigation
Jump to search
| (3 intermediate revisions by one other user not shown) | |||
| Line 1: | Line 1: | ||
== 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 [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
- 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.