Assume-guarantee reasoning with scheduled components
Opened this issue · 2 comments
What?
This extends AGREE to perform assume-guarantee reasoning with scheduled components.
Why?
AGREE assumes a synchronous model of computation. All components run in parallel simultaneously. This work incorporates an execution schedule in the assume-guarantee reasoning, which more accurately reflects the behavior of the system implementation.
How?
Modify the translation of AGREE AADL annex to Lustre model. All changes are in the "Main" node. No changes are made to the "Component" node.
- Add a new "circular counter" node definition, needed for schedule model
- Add a new "interval/between" node definition, needed for component input freeze assumption
- Add a schedule model, which defines "dispatch" and "complete" events
- Add top-level input freeze assumptions, needed for scheduling semantics
- Augment top-level contracts, needed for scheduling semantics
5.1. Assumption holds @ dispatch
5.2. Guarantee holds @ complete - Clock each component node instance with its complete event: condact (node_complete, node(…), true)
- Add component input freeze assumptions, a proof obligation
- Add component output freeze guarantees, needed for scheduling semantics
- Add component local variable freeze guarantees, otherwise trace shows random value while inactivated.
- Add component assumption freeze guarantees, otherwise trace shows random value while inactivated.
Right now, we only support AADL data ports and event/event data ports of size one, i.e. no FIFO semantics. Not so sure of scalability. But my tuition is that it should scale well, as we did not add anything complicated. Details can be found in our paper recently submitted for NFM 2022. The prototype implementation in Python and examples can be found here: https://github.com/loonwerks/Examples/tree/main/AGREE_Scheduled_Components
Note that for the "uav" example, the majority of the time (6-7 min) is spent on "consistence" check, the "property" check takes about 1-2 min.