How I can prove the correctness of a property using OSATE

[Faten Fakhfakh]

Hello,
I used OSATE to specify a model with AADL.
Now I need to prove the correctness of some properties relating to my system.
Property Example : In my system (vehicular system), we can never find 4 green lights
in an intersection.
I would like to know, how I can ensure that a property is verified or not with OSATE?
Please, describe the steps to follow.
Thank you for answering me.

[Brian Larson]

OSATE itself does not verify behavior.

For that you need AGREE, BLESS, or GUMBO.

AGREE and BLESS  can be installed with Help > Install Additional AADL Components.

For GUMBO you will need to install Sireum from Kansas State University and run from sources.

AGREE uses model checking for verification.  

If the property you want to verify can be expressed in LTL, AGREE would be a good choice.

GUMBO uses SMT solvers for verification.

If the property you want to verify is arithmetical, GUMBO would be a good choice.

BLESS uses an expressive temporal logic for specification which includes quantification over time.

However, BLESS produces human-readable deductive proofs for verification which requires human selection of tactics for the BLESS Proof Assistant.

Search GitHub for "BLESS-models" for example AADL projects having BLESS specifications, behaviors and proofs.

Look first at the "VVI" project.  

The "BLESS Book" is posted at multitude.net for LRM definition of BLESS grammar and formal semantics.

[Brian Larson]

You can use an installer for Sireum rather than sources:  https://sireum.org/getting-started/

[Faten Fakhfakh]

Hello,
I tried to install Sireum https://sireum.org/getting-started/
But, I encountered a lot of problems.
Was it abandoned? 

Actually, some files have been deleted (like project.cmd), but I need them for the steps in the command prompt...

I tried to download the file and integrate it manually, but the issue is not resolved.

--
You received this message because you are subscribed to a topic in the Google Groups "OSATE" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/osate/I_p87bo_0H4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to osate+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/osate/0faea077-823a-406d-94f8-9a3e780ee24an%40googlegroups.com.

[Jason Belt]

Hi Faten,

I'm a developer of HAMR which is a submodule of Sireum.  I just tried both installation techniques listed at https://sireum.org/getting-started/ (ie. "Using Installer Scripts" and "Git Source Distribution") in a Windows 11 ARM VM and both succeeded without incident.  The last line in your screenshot, ie "Could not execute command: .... art\bin\project.cmd json" hints that you're doing a Git Source installation.  I followed the "Using a NTFS partition ..." instructions (so enabled developer mode and long path support) so perhaps there's an issue with the WSL approach.  Could you post this as an issue to https://github.com/sireum/kekinian/issues with any additional feedback that you think might be helpful?

Regards,

Jason

You received this message because you are subscribed to the Google Groups "OSATE" group.
To unsubscribe from this group and stop receiving emails from it, send an email to osate+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/osate/CALsOKCLpYwGEZbonjHhv-LkrwOX0ze9tvD%3DdiSz%3DYfX037LQxA%40mail.gmail.com.