Assume-guarantee reasoning with scheduled components

[cong-liu-2000]

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.

1. Add a new "circular counter" node definition, needed for schedule model
2. Add a new "interval/between" node definition, needed for component input freeze assumption
3. Add a schedule model, which defines "dispatch" and "complete" events
4. Add top-level input freeze assumptions, needed for scheduling semantics
5. Augment top-level contracts, needed for scheduling semantics
   5.1. Assumption holds @ dispatch
   5.2. Guarantee holds @ complete
6. Clock each component node instance with its complete event: condact (node_complete, node(…), true)
7. Add component input freeze assumptions, a proof obligation
8. Add component output freeze guarantees, needed for scheduling semantics
9. Add component local variable freeze guarantees, otherwise trace shows random value while inactivated.
10. Add component assumption freeze guarantees, otherwise trace shows random value while inactivated.

[mwwhalen]

Wow, this is a big deal! Just curious, how well does it scale? Mike

…

On Thu, Jan 27, 2022 at 1:51 PM cong-liu-2000 ***@***.***> wrote: 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. 1. Add a new "circular counter" node definition, needed for schedule model 2. Add a new "interval/between" node definition, needed for component input freeze assumption 3. Add a schedule model, which defines "dispatch" and "complete" events 4. Add top-level input freeze assumptions, needed for scheduling semantics 5. Augment top-level contracts, needed for scheduling semantics 5.1. Assumption holds @ dispatch 5.2. Guarantee holds @ complete 6. Clock each component node instance with its complete event: condact (node_complete, node(…), true) 7. Add component input freeze assumptions, a proof obligation 8. Add component output freeze guarantees, needed for scheduling semantics 9. Add component local variable freeze guarantees, otherwise trace shows random value while inactivated. 10. Add component assumption freeze guarantees, otherwise trace shows random value while inactivated. — Reply to this email directly, view it on GitHub <#72>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABHZVOQ6K6M74GHTSKMBZH3UYGO3JANCNFSM5M64MJLQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

-- Michael Whalen Cell: 651-442-8834

[cong-liu-2000]

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.