Resolute allows users to define a set of claim functions and associate them with an AADL model. You can use these claim functions to represent the requirements to be satisfied, the verification actions used to verify them, and assumptions made by a verification action in order to produce a valid result. You will express the requirements as predicates on subrequirements and verification actions. Verification actions invoke Boolean computational functions to represent predicates to be evaluated and general computational functions to compute values to be compared in predicates. The computational function notation has its roots in Lute and REAL. You can organize claim functions into a hierarchy where a claim function is satisfied only if its subclaim functions are satisfied according to the specified predicate logic.
With the Resolute tool, users define claim functions and computational functions in Resolute annex libraries, i.e., Resolute annex clauses placed directly in an AADL package. The verification results are then displayed in a view labeled Assurance Case.
This tool is owned and licensed by Collins Aerospace. A BSD-like 3-clause license is described in the LICENSE file.
Development in Resolute takes place on two main branches: 'master' and 'stable.' The 'master' branch is the leading edge of development of Resolute and it maintains compatibility with the OSATE master branch. Developers are encouraged to create branches from the Resolute master branch to implement new features, address issues, or fix bugs. Once these branch developments are ready, they may be merged into the master branch. ATO be ready for merging onto the master branch, work must not break build or regression testing, must be deemed ready for use by the developmental users, and should have a suite of test cases.
The Resolute 'stable' branch contains the releases of Resolute (since Resolute 2.7.1). At time for releases, the progress on the master branch is merged onto the stable branch. At this point progress on the master must be ready for release to the public user community via a marked release in GitHub.
The Resolute tool development occurs mainly on the master branch of this repository. The 'master' branch contains the releases and the HEAD of this branch should contain the latest release. Individual development efforts should be completed on branches from the master branch and then merged back into the master via a pull request including informal peer review.
It is the general policy to consider releases as final; no updates to releases are made. Instead all updates are made to the master branch and incorporated into the next release.
Occasionally, it is desirable to create additional special-purpose branches for responding to issue/bug reports. These should be made from a branch from the release point, and if possible, merged onto the master branch prior to completion of the next release cycle. If such a branch spans a release, the developer should be merge the updated master branch onto the special-purpose branch to capture the updated versioning information and to avoid conflicts merging back into the develop branch.
Branch names should be chosen to describe the activity to be taken on the branch. For example, to develop a new feature 'A', the branch might be named 'develop-feature-A.' Or to fix an issue recorded in the issue base the branch might be named 'fix-issue-x' where x is the sequence number assigned to the issue.
Tags are typically reserved for releases, but may be used to mark special points in the development process (i.e. snapshot tags).
The CI/CD pipeline is carried out via GitHub actions. There are three different workflows defined. They are as follows:
mvn clean verify
mvn verify -Pbuild-snapshot
mvn verify -Pbuild-release
Important Details about Snapshot Tags
git tag x.x.x.yyyyMMddHHmm-SNAPSHOT
git push origin x.x.x.yyyyMMddHHmm-SNAPSHOT
Important Details about Release Tags
git tag x.x.x-RELEASE
git push origin x.x.x-RELEASE