PV3 ⊧ AGREE: Assume Guarantee Reasoning Environmentchecks properties against an AADL model

Application domain/field

• Model checking
• Cyber-physical systems
• System design verification
• Assume-guarantee contracts

Type of tool

Model checker

Expected input

AADL model

Format:

.aadl file

Expected output

Per property it indicates whether it could be verified in the GUI. If it could not be verified there the user can view a counterexample that demonstrates the failure.

Internals

• Infinite-state model checker.
• Can analyse systems with real-valued variables.
• Translates an AADL model and the corresponding contracts into Lustre, then uses JKind for the back-end analysis.
• Uses Z3, JKind