Portal:Tutorials
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
- 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.