search

loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

Assume-guarantee reasoning with scheduled components #72

Open cong-liu-2000 opened 2 years ago

cong-liu-2000 commented 2 years ago

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 commented 2 years ago

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 https://github.com/loonwerks/AGREE/issues/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 commented 2 years ago

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.