Modeling and Verification of Real-Time Systems with the Event Calculus and s(CAS

on YouTube ↗26m

" summary

Models the Train-Gate-Controller in Event Calculus encoded for s(CASP), using CLP(R) so dense time and continuous positions/angles require no discretization and are handled via constraint solving over reals. Queries check safety (gate closed when train between markers at 10 and 20) and liveness (opened by time 30) under parameterized speeds (train = 1 unit/s) and gate rates; counterexamples appear when lowering or rising rates are too slow. Verification is query-driven and returns results in seconds, demonstrating fast runtimes and supporting abduction for missed hazard assumptions.

AI-written summary · about

" chapters (8)

1. 0:00Start
2. 1:49Timed Automata Approach
3. 3:17Axioms for Basic Event Calculus
4. 4:53Model Dependent Fluids
5. 9:31The Train Gate Controller
6. 11:09Event Driven Requirements
7. 16:14Derived Fluids
8. 21:12Conclusion