Difference between revisions of "Main Page"

From Ivoire
Jump to navigation Jump to search
(Add picture of team meeting)
 
(7 intermediate revisions by the same user not shown)
Line 1: Line 1:
 +
[[File:IVOIRE Meeting 2024 Düsseldorf.jpg|thumb|right|The [[Ivoire:About#People|IVOIRE team]] meeting in Düsseldorf]]
 +
 
Welcome to the IVOIRE homepage. Here we keep information about the project, the current status, our publications and the people behind the project.
 
Welcome to the IVOIRE homepage. Here we keep information about the project, the current status, our publications and the people behind the project.
  
 +
== News ==
  
 +
* '''25 June 2024''' (upcoming) - The [[IVOIRE Workshop 2024]] will take place at [https://abz-conf.org/site/2024 ABZ 2024] in Bergamo, Italy.
 +
* '''2 May 2024''' - Project meeting was held in Düsseldorf, Germany.
 +
* '''February 2024''' - Article "[https://www.sciencedirect.com/science/article/pii/S2352220824000014?via%3Dihub Trace preservation in B and Event-B refinements]" by Stock et al. was published in [https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/137/suppl/C JLAMP Volume 137].
 +
* '''November 2023''' - Sebastian Stock presented the papers "[https://link.springer.com/chapter/10.1007/978-981-99-7584-6_16 Early and Systematic Validation of Formal Models]" and "[https://link.springer.com/chapter/10.1007/978-981-99-7584-6_12 Validation-Driven Development]" at [https://formal-analysis.com/icfem/2023/ ICFEM 2023] in Brisbane, Australia.
 +
* '''June 2023''' - Geleßus, Stock, and Vu presented multiple IVOIRE-related papers at [https://abz2023.loria.fr/ ABZ 2023] in Nancy, France.
 +
* '''30 May 2023''' - The [[IVOIRE Workshop 2023]] took place at [https://abz2023.loria.fr/ ABZ 2023] in Nancy, France.
 +
* '''October 2022''' - Stock and Vu presented multiple IVOIRE-related papers at [https://maude.ucm.es/ICFEM22/ ICFEM 2022] in Madrid, Spain.
 +
* '''September 2022''' - Fabian Vu presented the paper "[https://link.springer.com/chapter/10.1007/978-3-031-15008-1_4 Generating Domain-Specific Interactive Validation Documents]" at [https://fmics2022.fsa.win.tue.nl/ FMICS 2022] in Warsaw, Poland.
 +
* '''August 2022''' - Sebastian Stock presented the paper "[https://link.springer.com/chapter/10.1007/978-3-031-14343-4_31 Application of Validation Obligations to Security Concerns]" at [https://www.dexa.org/previous/dexa2022/www.dexa.org/ DEXA 2022] in Vienna, Austria.
 +
* '''7 June 2022''' - The [[IVOIRE Workshop 2022]] took place at [https://ifm22.si.usi.ch/ iFM 2022] in Lugano, Switzerland.
  
−
=== The IVOIRE Idea ===
+
== The IVOIRE Idea ==
  
 
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 on 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.
 
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 on 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.
Line 12: Line 25:
  
  
 +
== Validation Obligations ==
 +
 +
 +
[[File:VTFunction.png|| 1000px]]
 +
 +
 +
Within the context of software engineering, it is vital to check whether a model meets its specification (verification) and requirements (validation). Various formal techniques exist to verify a requirements model, such as theorem proving or model checking. However, only a few formal techniques are at our disposal to validate a requirements model. In this report, we introduce a new technique with validation obligations (VOs) alongside existing proof obligations (POs) to check the compliance of a model with its requirements. A VO is composed of (multiple) validation tasks (VT) associated with a model to check its compliance with a particular requirement (formalized as VO_{id} : VO_{predicate}). The validation predicate applies the validation function on the VTs the corresponding VO is composed of. A validation task (VT) is identified with an identifier, and consists of a validation technique that is applied with the given validation parameters to the corresponding context (formalized as <math>VT_{id}/VT_{context}/VT_{technique}: VT_{parameters})</math>. Finally, this report demonstrates the usability of the VO approach on a simple Traffic Light example. Another important aspect is the traceability of VOs to their VTs and requirements. As shown in the Figure above, one can, e.g., see that VO18 could be traced to OCT1, TR1, TR2, and COV1, SCENARIO1, and SCENARIO2, and thus also VO12 and VO13 if it fails.
  
−
Within the context of software engineering, it is vital to check whether a model meets its specification (verification) and requirements (validation). Various formal techniques exist to verify a requirements model, such as theorem proving or model checking. However, only a few formal techniques are at our disposal to validate a requirements model. In this report, we introduce a new technique with validation obligations (VOs) alongside existing proof obligations (POs) to check the compliance of a model with its requirements. A VO is composed of (multiple) validation tasks (VT) associated with a model to check its compliance with a particular requirement (formalized as VO_{id} : VO_{predicate}). The validation predicate applies the validation function on the VTs the corresponding VO is composed of. A validation task (VT) is identified with an identifier, and consists of a validation technique that is applied with the given validation parameters to the corresponding context (formalized as VT_{id}/VT_{context}/VT_{technique}: VT_{parameters}). Finally, this report demonstrates the usability of the VO approach on a simple Traffic Light example. Another important aspect is the traceability of VOs to their VTs and requirements. As shown in the Figure above, one can, e.g., see that VO18 could be traced to OCT1, TR1, TR2, and COV1, SCENARIO1, and SCENARIO2, and thus also VO12 and VO13 if it fails.
+
<math>a</math>
 +
<math>VT_{id}/VT_{context}/VT_{technique}: VT_{parameters})</math>

Latest revision as of 08:49, 13 May 2024

The IVOIRE team meeting in Düsseldorf

Welcome to the IVOIRE homepage. Here we keep information about the project, the current status, our publications and the people behind the project.

News

The IVOIRE Idea

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 on the Ivoire:About page. For a first deep dive into the VO semantic, see the paper that introduces IVOIRE.


RefinementHierarchy.png


Validation Obligations

VTFunction.png


Within the context of software engineering, it is vital to check whether a model meets its specification (verification) and requirements (validation). Various formal techniques exist to verify a requirements model, such as theorem proving or model checking. However, only a few formal techniques are at our disposal to validate a requirements model. In this report, we introduce a new technique with validation obligations (VOs) alongside existing proof obligations (POs) to check the compliance of a model with its requirements. A VO is composed of (multiple) validation tasks (VT) associated with a model to check its compliance with a particular requirement (formalized as VO_{id} : VO_{predicate}). The validation predicate applies the validation function on the VTs the corresponding VO is composed of. A validation task (VT) is identified with an identifier, and consists of a validation technique that is applied with the given validation parameters to the corresponding context (formalized as <math>VT_{id}/VT_{context}/VT_{technique}: VT_{parameters})</math>. Finally, this report demonstrates the usability of the VO approach on a simple Traffic Light example. Another important aspect is the traceability of VOs to their VTs and requirements. As shown in the Figure above, one can, e.g., see that VO18 could be traced to OCT1, TR1, TR2, and COV1, SCENARIO1, and SCENARIO2, and thus also VO12 and VO13 if it fails.

<math>a</math> <math>VT_{id}/VT_{context}/VT_{technique}: VT_{parameters})</math>

Retrieved from "https://isse.jku.at/ivoire/index.php?title=Main_Page&oldid=208"