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.