Difference between revisions of "Main Page"
| Line 8: | Line 8: | ||
With these VOs it then shall be possible to show whether a certain behavior is present in a formal model. | With these VOs it then shall be possible to show whether a certain behavior is present in a formal model. | ||
By showing if a property is present one can reason about the model and explain the features to its stakeholders. | By showing if a property is present one can reason about the model and explain the features to its stakeholders. | ||
| − | VOs will enrich the modeling process in formal methods as shown in the picture above. While the normal refinement chain M0-M2 is already present we plan to introduce VOs (green boxes) and various views for the model ( | + | VOs will enrich the modeling process in formal methods as shown in the picture above. While the normal refinement chain M0-M2 is already present we plan to introduce VOs (green boxes) and various views for the model (blue boxes). The progress can be followed in detail in the [[Ivoire:About]] page. |
For a first deep dive into the VO semantic see the [https://arxiv.org/abs/2102.06037 paper] that introduces IVOIRE. | For a first deep dive into the VO semantic see the [https://arxiv.org/abs/2102.06037 paper] that introduces IVOIRE. | ||
Revision as of 13:37, 29 November 2021
Welcome to the IVOIRE homepage. Here we keep information about the project, the current status, our publications and the people behind the project.
The IVOIRE project aims to introduce so-called Validation Obligations (VOs) into formal methods.
With these VOs it then shall be possible to show whether a certain behavior is present in a formal model.
By showing if a property is present one can reason about the model and explain the features to its stakeholders.
VOs will enrich the modeling process in formal methods as shown in the picture above. While the normal refinement chain M0-M2 is already present we plan to introduce VOs (green boxes) and various views for the model (blue boxes). The progress can be followed in detail in the Ivoire:About page.
For a first deep dive into the VO semantic see the paper that introduces IVOIRE.
