Help with Resolute Verification Methods in ALISA – Errors in Assurance View

[Yara Hallak]

Hello everyone,

I am a beginner with the OSATE platform and have just started using AADL, Resolute, and ALISA.

I am currently trying to implement a method to check if an AADL model covers all requirements. For that, I am using ALISA and Resolute to develop the methods used in the .verify files to check requirements.

Here is a summary of my setup:

• .aadl file:

package packageName

public

annex Resolute {**

NameXX(comp: component):{feature} =

features(comp)

... more resolute functions

• .methodregistry file where I defined the verification methods using the Resolute functions:

verification methods resolute [

method M1(component):

"description..."[

resolute PackageName.PackageName_public.Resolute.Resolute.NameXX

]

... more

• .verify file:
  I defined the verification plan (VP) and the claims using the verification methods. Each VP is associated with a requirements set, and each claim verifies a requirement. These VPs are then used by the assurance case → assurance plans.

Problem:
When running the assurance case in the Assurance View of OSATE, I keep getting errors (attached). I am not able to debug or identify the root cause. I have followed the available documentation as closely as possible while writing the code.

If anyone has experience with Resolute functions in ALISA, or has encountered similar problems, I would greatly appreciate any guidance or advice.

Thank you very much in advance!

Best regards,

[Sam Procter]

Hello Yara Hallak,

 

This looks like a bug – could you file it as a bug report at https://github.com/osate/osate2/issues?

 

It would be ideal if you could create a minimal reproducible example (some advice here if you’re not familiar with the term: https://stackoverflow.com/help/minimal-reproducible-example) as part of that, as it will help us diagnose and hopefully fix the issue.

 

Thank you!

 

Yours truly,

Sam Procter

 

From: os...@googlegroups.com <os...@googlegroups.com> on behalf of Yara Hallak <yarah...@gmail.com>
Date: Tuesday, August 26, 2025 at 8:10 AM
To: OSATE <os...@googlegroups.com>
Subject: [OSATE] Help with Resolute Verification Methods in ALISA – Errors in Assurance View

Warning: External Sender - do not click links or open attachments unless you recognize the sender and know the content is safe.

 

--
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 visit https://groups.google.com/d/msgid/osate/586b8700-9bc2-481b-b247-2b6ec49d96c7n%40googlegroups.com.

[Yara Hallak]

Hello,

Thank you for your reply.

I even tried to verify the requirements in the assurance case of the alisa ISOLETTE project example, but I got the same error message on all the claims that are not to check "predicates".

I thought that it was from my project but since it is not even working on the predefined examples, it might be something else, which I still couldn't figure. 

Thank you

[John Hudak]

Hello Yara

If the tools in the Isolette example are the same that you want to use and what you are trying to do e.g. Alyssa, resolute, etc., I suggest you try to build The Isolette example with the same version of OSATE,  Alyssa and resolute that was used in the example.

If I recall correctly, the isolate example was verified to work about three or four years ago so you will have to go back a number of versions of those tools to try to make it work.

Most of the examples were not reverified with each newer version of OSATE and resolute.

You should also try to send an email to the resolute maintainers at loon works to see if they can quickly identify the issue

Coming up with a minimal example with the versions you are using now would be very helpful to diagnose any potential issue with the current tool versions

Good luck

To view this discussion visit https://groups.google.com/d/msgid/osate/25a8d406-7556-40d5-965d-d26a51d38ffan%40googlegroups.com.