Verification of the Anti-lock Braking System(ABS)

Mainly based on the paper: <Periodic scheduling for MARTE/CCSL: Theory and practice> & <Verifying MARTE/CCSL Mode Behaviors Using UPPAAL>

Main Work

1. Model the ABS via CCSL(See PPT).
2. Verify whether the generated data satisfies the constraints.
3. Whether deadlock will happen under the constraints.