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

Application domain/field

Type of tool

Model checker

Expected input

AADL model


.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.


AADL Model checking


Related papers

Last publication date

September 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.