ADVANCE D3.2 General Platform Maintenance: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
Initial version to be filled
 
imported>Ladenberger
Line 48: Line 48:


=== Overview ===
=== Overview ===
{{TODO|Fill this paragraph.}}
{{TODO|Fill this paragraph.}}


=== Motivations / Decisions ===
=== Motivations / Decisions ===
{{TODO|Fill this paragraph.}}
{{TODO|Fill this paragraph.}}
Traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. In <ref name="req1ref">http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref>, we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W ∧ S ⇒ R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts. We created tool support for this approach by integrating Rodin and ProR. We designed it with the goal to support the approach described in <ref name="req1ref"/>, and to ease the integration of natural language requirements and Event-B.


=== Available Documentation ===
=== Available Documentation ===
Line 59: Line 63:
{{TODO|Fill this paragraph.}}
{{TODO|Fill this paragraph.}}


 
== References ==
<references/>


== Camille (Ingo Weigelt) ==
== Camille (Ingo Weigelt) ==

Revision as of 14:26, 14 June 2012

Core Rodin platform (Thomas Muller)

Overview

TODO: Fill this paragraph.

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.


UML-B Improvements (Colin Snook, Vitaly Savicks)

Overview

TODO: Fill this paragraph.

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.

Code generation (Andy Edmunds)

Overview

TODO: Fill this paragraph.

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.


ProR (Michael Jastram/Lukas Ladenberger)

Overview

TODO: Fill this paragraph.

Motivations / Decisions

TODO: Fill this paragraph.

Traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. In [1], we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W ∧ S ⇒ R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts. We created tool support for this approach by integrating Rodin and ProR. We designed it with the goal to support the approach described in [1], and to ease the integration of natural language requirements and Event-B.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.

References

Camille (Ingo Weigelt)

Overview

TODO: Fill this paragraph.

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.

References